chiark / gitweb /
topbloke-formulae.git
5 years agostrategy: new, wip, notational fixes
Ian Jackson [Sun, 27 May 2012 17:57:16 +0000 (18:57 +0100)]
strategy: new, wip, notational fixes

5 years agostrategy: new, wip, notational fixes
Ian Jackson [Sun, 27 May 2012 17:43:47 +0000 (18:43 +0100)]
strategy: new, wip, notational fixes

5 years agostrategy: new, wip, found
Ian Jackson [Sun, 27 May 2012 17:24:09 +0000 (18:24 +0100)]
strategy: new, wip, found

5 years agostrategy: new, wip
Ian Jackson [Sun, 13 May 2012 12:59:43 +0000 (13:59 +0100)]
strategy: new, wip

5 years agostrategy: new, wip
Ian Jackson [Sat, 12 May 2012 10:15:42 +0000 (11:15 +0100)]
strategy: new, wip

5 years agostrategy: new, wip
Ian Jackson [Fri, 11 May 2012 23:41:30 +0000 (00:41 +0100)]
strategy: new, wip

5 years agostrategy: new, wip
Ian Jackson [Fri, 11 May 2012 23:29:26 +0000 (00:29 +0100)]
strategy: new, wip

5 years agostrategy: new, wip
Ian Jackson [Fri, 11 May 2012 23:21:12 +0000 (00:21 +0100)]
strategy: new, wip

5 years agostrategy: wip
Ian Jackson [Tue, 1 May 2012 13:21:53 +0000 (14:21 +0100)]
strategy: wip

5 years agostrategy: wip
Ian Jackson [Mon, 30 Apr 2012 10:30:46 +0000 (11:30 +0100)]
strategy: wip

5 years agostrategy: wip
Ian Jackson [Sun, 29 Apr 2012 22:27:24 +0000 (23:27 +0100)]
strategy: wip

5 years agostrategy: wip
Ian Jackson [Sun, 29 Apr 2012 22:25:08 +0000 (23:25 +0100)]
strategy: wip

5 years agostrategy: wip
Ian Jackson [Sun, 29 Apr 2012 21:31:10 +0000 (22:31 +0100)]
strategy: wip

5 years agostrategy: wip
Ian Jackson [Fri, 27 Apr 2012 13:31:25 +0000 (14:31 +0100)]
strategy: wip

5 years agostrategy: rename \gref macros: perl -i~ -pe 's/gref([zcuf])/tip$1/g' *.tex
Ian Jackson [Fri, 27 Apr 2012 12:57:21 +0000 (13:57 +0100)]
strategy: rename \gref macros: perl -i~ -pe 's/gref([zcuf])/tip$1/g' *.tex

5 years agostrategy: wip
Ian Jackson [Fri, 27 Apr 2012 12:56:04 +0000 (13:56 +0100)]
strategy: wip

5 years agostrategy: wip
Ian Jackson [Fri, 27 Apr 2012 12:31:59 +0000 (13:31 +0100)]
strategy: wip

5 years agostrategy: wip
Ian Jackson [Fri, 27 Apr 2012 11:51:59 +0000 (12:51 +0100)]
strategy: wip

5 years agoinvariants: remove some slightly ugly colons
Ian Jackson [Fri, 27 Apr 2012 11:51:52 +0000 (12:51 +0100)]
invariants: remove some slightly ugly colons

5 years agostrategy: wip, notation changes, finished planning we think
Ian Jackson [Fri, 27 Apr 2012 11:22:19 +0000 (12:22 +0100)]
strategy: wip, notation changes, finished planning we think

5 years agonotation: change >_1 to >_1: so we can define \succ_1 slightly differently
Ian Jackson [Fri, 27 Apr 2012 11:22:01 +0000 (12:22 +0100)]
notation: change >_1 to >_1: so we can define \succ_1 slightly differently

5 years agostrategy: use \chapter
Ian Jackson [Fri, 27 Apr 2012 10:19:51 +0000 (11:19 +0100)]
strategy: use \chapter

5 years agostrategy: wip
Ian Jackson [Thu, 26 Apr 2012 00:04:53 +0000 (01:04 +0100)]
strategy: wip

5 years agostrategy: wip
Ian Jackson [Wed, 25 Apr 2012 22:06:25 +0000 (23:06 +0100)]
strategy: wip

5 years agostrategy: wip
Ian Jackson [Wed, 25 Apr 2012 21:14:11 +0000 (22:14 +0100)]
strategy: wip

5 years agostrategy: wip
Ian Jackson [Tue, 24 Apr 2012 00:41:07 +0000 (01:41 +0100)]
strategy: wip

5 years agostrategy: provide new \pc eg al
Ian Jackson [Tue, 24 Apr 2012 00:40:51 +0000 (01:40 +0100)]
strategy: provide new \pc eg al

5 years agomerge: fix dependency reinsertion blurb to mention the need for the base to be merged...
Ian Jackson [Wed, 18 Apr 2012 20:44:08 +0000 (21:44 +0100)]
merge: fix dependency reinsertion blurb to mention the need for the base to be merged first

5 years agounique tips: rename anticommit condition Unique Tip to Correct Tip
Ian Jackson [Wed, 18 Apr 2012 20:38:36 +0000 (21:38 +0100)]
unique tips: rename anticommit condition Unique Tip to Correct Tip

5 years agounique tips: fix various \pendsof and \pancsof to refer to \py not \p
Ian Jackson [Wed, 18 Apr 2012 20:37:05 +0000 (21:37 +0100)]
unique tips: fix various \pendsof and \pancsof to refer to \py not \p

5 years agounique tips: add condition and prove, for merge
Ian Jackson [Wed, 18 Apr 2012 20:34:13 +0000 (21:34 +0100)]
unique tips: add condition and prove, for merge

5 years agoprovide \bigexists
Ian Jackson [Wed, 18 Apr 2012 20:33:53 +0000 (21:33 +0100)]
provide \bigexists

5 years agounique tips: single parent unique tips applies to anticommit too
Ian Jackson [Wed, 18 Apr 2012 20:11:25 +0000 (21:11 +0100)]
unique tips: single parent unique tips applies to anticommit too

5 years agounique tips: single parent unique tips use cases
Ian Jackson [Wed, 18 Apr 2012 17:33:22 +0000 (18:33 +0100)]
unique tips: single parent unique tips use cases

5 years agounique tips: single parent unique tips lemma
Ian Jackson [Wed, 18 Apr 2012 17:27:03 +0000 (18:27 +0100)]
unique tips: single parent unique tips lemma

5 years agounique tips: add to list of invariants
Ian Jackson [Wed, 18 Apr 2012 17:18:09 +0000 (18:18 +0100)]
unique tips: add to list of invariants

5 years agofix typo f0.3
Ian Jackson [Tue, 27 Mar 2012 20:24:35 +0000 (21:24 +0100)]
fix typo

5 years agocomments from mdw - fix incorrect refs to B in create tip
Ian Jackson [Tue, 27 Mar 2012 19:07:00 +0000 (20:07 +0100)]
comments from mdw - fix incorrect refs to B in create tip

5 years agocomments from mdw - add note re universal quantification
Ian Jackson [Tue, 27 Mar 2012 18:17:34 +0000 (19:17 +0100)]
comments from mdw - add note re universal quantification

5 years agocomments from mdw - add section on \set to notation
Ian Jackson [Tue, 27 Mar 2012 18:14:20 +0000 (19:14 +0100)]
comments from mdw - add section on \set to notation

5 years agocomments from mdw - clarify that \p are disjoint by construction
Ian Jackson [Tue, 27 Mar 2012 18:14:08 +0000 (19:14 +0100)]
comments from mdw - clarify that \p are disjoint by construction

5 years agoclarify proof of calculation of ends
Ian Jackson [Mon, 26 Mar 2012 00:19:13 +0000 (01:19 +0100)]
clarify proof of calculation of ends

5 years agofix notation in calculation of ends
Ian Jackson [Mon, 26 Mar 2012 00:17:32 +0000 (01:17 +0100)]
fix notation in calculation of ends

5 years agoadd final.ps to default target
Ian Jackson [Sun, 25 Mar 2012 20:02:44 +0000 (21:02 +0100)]
add final.ps to default target

5 years agoclarify merge complex D=C
Ian Jackson [Sun, 25 Mar 2012 20:02:02 +0000 (21:02 +0100)]
clarify merge complex D=C

5 years agoget rid of a leftover spurious \neg[]
Ian Jackson [Sun, 25 Mar 2012 19:48:22 +0000 (20:48 +0100)]
get rid of a leftover spurious \neg[]

5 years agofix leftover \land
Ian Jackson [Sun, 25 Mar 2012 19:45:56 +0000 (20:45 +0100)]
fix leftover \land

5 years agocommentary about exhaustiveness
Ian Jackson [Sun, 25 Mar 2012 19:45:06 +0000 (20:45 +0100)]
commentary about exhaustiveness

5 years ago\nothaspatch with two slashes again as it's not equivalent to \neg \haspatch; partial...
Ian Jackson [Sun, 25 Mar 2012 19:41:28 +0000 (20:41 +0100)]
\nothaspatch with two slashes again as it's not equivalent to \neg \haspatch; partial revert of d00298b5b6d70bd919824ab8b79d71663f3cdfa6

5 years agorefactor for coherence cases - merge
Ian Jackson [Wed, 21 Mar 2012 21:47:29 +0000 (21:47 +0000)]
refactor for coherence cases - merge

5 years agorefactor for coherence cases - simple, fix leftover ~
Ian Jackson [Wed, 21 Mar 2012 21:44:57 +0000 (21:44 +0000)]
refactor for coherence cases - simple, fix leftover ~

5 years agorefactor for coherence cases - anticommit
Ian Jackson [Wed, 21 Mar 2012 21:42:22 +0000 (21:42 +0000)]
refactor for coherence cases - anticommit

5 years agofix wrong symbols in simple
Ian Jackson [Wed, 21 Mar 2012 21:37:38 +0000 (21:37 +0000)]
fix wrong symbols in simple

5 years agorefactor for coherence cases - simple, more
Ian Jackson [Wed, 21 Mar 2012 21:37:25 +0000 (21:37 +0000)]
refactor for coherence cases - simple, more

5 years agorefactor for coherence cases - simple
Ian Jackson [Wed, 21 Mar 2012 21:34:24 +0000 (21:34 +0000)]
refactor for coherence cases - simple

5 years agowip exclusive haspatch - clarify Merge Coherence (for neither haspatch)
Ian Jackson [Wed, 21 Mar 2012 21:26:03 +0000 (21:26 +0000)]
wip exclusive haspatch - clarify Merge Coherence (for neither haspatch)

5 years agowip exclusive haspatch - fix Merge Coherence (for disagree)
Ian Jackson [Wed, 21 Mar 2012 21:25:48 +0000 (21:25 +0000)]
wip exclusive haspatch - fix Merge Coherence (for disagree)

5 years agowip exclusive haspatch - fix Merge Coherence (for both haspatch)
Ian Jackson [Wed, 21 Mar 2012 21:25:27 +0000 (21:25 +0000)]
wip exclusive haspatch - fix Merge Coherence (for both haspatch)

5 years agowip exclusive haspatch - fix Anticommit
Ian Jackson [Wed, 21 Mar 2012 21:08:28 +0000 (21:08 +0000)]
wip exclusive haspatch - fix Anticommit

5 years agowip exclusive haspatch - fix Anticommit wip
Ian Jackson [Wed, 21 Mar 2012 18:36:31 +0000 (18:36 +0000)]
wip exclusive haspatch - fix Anticommit wip

5 years agowip exclusive haspatch - fix Create Tip
Ian Jackson [Wed, 21 Mar 2012 18:34:38 +0000 (18:34 +0000)]
wip exclusive haspatch - fix Create Tip

5 years agowip exclusive haspatch - fix Create Base
Ian Jackson [Wed, 21 Mar 2012 18:29:47 +0000 (18:29 +0000)]
wip exclusive haspatch - fix Create Base

5 years agosimple - improve title cap
Ian Jackson [Wed, 21 Mar 2012 18:28:07 +0000 (18:28 +0000)]
simple - improve title cap

5 years agowip exclusive haspatch - fix Simple / Coherence
Ian Jackson [Wed, 21 Mar 2012 18:26:35 +0000 (18:26 +0000)]
wip exclusive haspatch - fix Simple / Coherence

5 years agosimple commit fix P notation
Ian Jackson [Wed, 21 Mar 2012 18:22:59 +0000 (18:22 +0000)]
simple commit fix P notation

5 years agowip exclusive haspatch - fix Commit Annotation
Ian Jackson [Wed, 21 Mar 2012 18:21:28 +0000 (18:21 +0000)]
wip exclusive haspatch - fix Commit Annotation

5 years agowip exclusive haspatch - fix Tip Own Contents
Ian Jackson [Wed, 21 Mar 2012 18:20:04 +0000 (18:20 +0000)]
wip exclusive haspatch - fix Tip Own Contents

5 years agowip exclusive haspatch - change notation to F in defn
Ian Jackson [Wed, 21 Mar 2012 18:17:15 +0000 (18:17 +0000)]
wip exclusive haspatch - change notation to F in defn

5 years agowip exclusive haspatch - reorder notation
Ian Jackson [Wed, 21 Mar 2012 18:16:42 +0000 (18:16 +0000)]
wip exclusive haspatch - reorder notation

5 years agowip exclusive haspatch - better kerning
Ian Jackson [Tue, 20 Mar 2012 18:03:23 +0000 (18:03 +0000)]
wip exclusive haspatch - better kerning

5 years agowip exclusive haspatch - better symbol
Ian Jackson [Tue, 20 Mar 2012 15:23:31 +0000 (15:23 +0000)]
wip exclusive haspatch - better symbol

5 years agowip exclusive haspatch - notation
Ian Jackson [Tue, 20 Mar 2012 15:10:19 +0000 (15:10 +0000)]
wip exclusive haspatch - notation

5 years agoswap L and R headers and footers, better for 2-up output etc.
Ian Jackson [Sun, 18 Mar 2012 11:46:51 +0000 (11:46 +0000)]
swap L and R headers and footers, better for 2-up output etc.

5 years agorevid - use "git foo" not "git-foo"
Ian Jackson [Sun, 18 Mar 2012 11:43:36 +0000 (11:43 +0000)]
revid - use "git foo" not "git-foo"

5 years agorevid - better deps
Ian Jackson [Sun, 18 Mar 2012 11:29:20 +0000 (11:29 +0000)]
revid - better deps

5 years agomake clean - remove *.ps
Ian Jackson [Sun, 18 Mar 2012 11:27:58 +0000 (11:27 +0000)]
make clean - remove *.ps

5 years agorevid - include
Ian Jackson [Sun, 18 Mar 2012 11:27:23 +0000 (11:27 +0000)]
revid - include

5 years agorevid - make more suitable for us
Ian Jackson [Sun, 18 Mar 2012 11:26:58 +0000 (11:26 +0000)]
revid - make more suitable for us

5 years ago.git-revid from my trains.git
Ian Jackson [Sun, 18 Mar 2012 11:15:28 +0000 (11:15 +0000)]
.git-revid from my trains.git

5 years agomore sophisticated makefile (make once etc.)
Ian Jackson [Sun, 18 Mar 2012 11:10:13 +0000 (11:10 +0000)]
more sophisticated makefile (make once etc.)

5 years agomerge coherence complex - remove unneeded ref to def of haspatch
Ian Jackson [Sun, 18 Mar 2012 11:00:01 +0000 (11:00 +0000)]
merge coherence complex - remove unneeded ref to def of haspatch

5 years agomerge coherence complex - fix proof intro re haspatch nonexclusivity
Ian Jackson [Sun, 18 Mar 2012 10:59:16 +0000 (10:59 +0000)]
merge coherence complex - fix proof intro re haspatch nonexclusivity

5 years agofix non-topbloke merges empty ends proof
Ian Jackson [Sun, 18 Mar 2012 10:55:40 +0000 (10:55 +0000)]
fix non-topbloke merges empty ends proof

5 years agorationalise patch notation names - anticommit
Ian Jackson [Sun, 18 Mar 2012 10:51:23 +0000 (10:51 +0000)]
rationalise patch notation names - anticommit

5 years agoprovide \pl etc.
Ian Jackson [Sun, 18 Mar 2012 10:51:07 +0000 (10:51 +0000)]
provide \pl etc.

5 years agorationalise patch notation names - annotations
Ian Jackson [Sun, 18 Mar 2012 10:44:03 +0000 (10:44 +0000)]
rationalise patch notation names - annotations

5 years agorename Tip Self Contents -> Tip Own Contents f0.2
Ian Jackson [Fri, 16 Mar 2012 23:47:45 +0000 (23:47 +0000)]
rename Tip Self Contents -> Tip Own Contents

5 years agorename Tip Self Inpatch -> Tip Self Contents
Ian Jackson [Fri, 16 Mar 2012 23:46:59 +0000 (23:46 +0000)]
rename Tip Self Inpatch -> Tip Self Contents

5 years agosmall fixes
Ian Jackson [Fri, 16 Mar 2012 23:45:16 +0000 (23:45 +0000)]
small fixes

5 years agonon-topbloke merges fix merge ends proof
Ian Jackson [Fri, 16 Mar 2012 23:39:37 +0000 (23:39 +0000)]
non-topbloke merges fix merge ends proof

5 years agobe more rigorous about conformance
Ian Jackson [Fri, 16 Mar 2012 23:14:18 +0000 (23:14 +0000)]
be more rigorous about conformance

5 years agoadd note about non-exclusivity of \haspatch and \nothaspatch
Ian Jackson [Fri, 16 Mar 2012 23:00:18 +0000 (23:00 +0000)]
add note about non-exclusivity of \haspatch and \nothaspatch

5 years agouse new extended Self Tip Inpatch
Ian Jackson [Fri, 16 Mar 2012 23:00:00 +0000 (23:00 +0000)]
use new extended Self Tip Inpatch

5 years agoextend Self Tip Inpatch
Ian Jackson [Fri, 16 Mar 2012 22:53:39 +0000 (22:53 +0000)]
extend Self Tip Inpatch

5 years agoremove a couple of spurious $\qed$
Ian Jackson [Fri, 16 Mar 2012 22:43:22 +0000 (22:43 +0000)]
remove a couple of spurious $\qed$

5 years agoremove spurious .
Ian Jackson [Fri, 16 Mar 2012 22:40:45 +0000 (22:40 +0000)]
remove spurious .

5 years agomerge fixes/clarifications - clarify and fix tip contents R \in \py
Ian Jackson [Fri, 16 Mar 2012 22:34:19 +0000 (22:34 +0000)]
merge fixes/clarifications - clarify and fix tip contents R \in \py

5 years agomerge fixes/clarifications - clarify tip contents R \not\in \py
Ian Jackson [Fri, 16 Mar 2012 22:28:31 +0000 (22:28 +0000)]
merge fixes/clarifications - clarify tip contents R \not\in \py

5 years agomerge fixes/clarifications - sort out complex case D = C
Ian Jackson [Fri, 16 Mar 2012 22:25:11 +0000 (22:25 +0000)]
merge fixes/clarifications - sort out complex case D = C

5 years agomerge fixes/clarifications - fix several P to \p
Ian Jackson [Fri, 16 Mar 2012 22:00:55 +0000 (22:00 +0000)]
merge fixes/clarifications - fix several P to \p