chiark / gitweb /
topbloke-formulae.git
7 years agoanticommit base acyclic
Ian Jackson [Sun, 11 Mar 2012 12:07:19 +0000 (12:07 +0000)]
anticommit base acyclic

7 years agostrengthen anticommit condition to From Base
Ian Jackson [Sun, 11 Mar 2012 12:06:57 +0000 (12:06 +0000)]
strengthen anticommit condition to From Base

7 years agomerge foreign inclusion
Ian Jackson [Sun, 11 Mar 2012 11:51:01 +0000 (11:51 +0000)]
merge foreign inclusion

7 years agomove alternative formulation of merge results into lemmas
Ian Jackson [Sun, 11 Mar 2012 11:48:14 +0000 (11:48 +0000)]
move alternative formulation of merge results into lemmas

7 years agoProve that plain git merges on non-tb branches are ok
Ian Jackson [Sun, 11 Mar 2012 11:24:26 +0000 (11:24 +0000)]
Prove that plain git merges on non-tb branches are ok

7 years agoMention that simple commit justification applies to tb export too
Ian Jackson [Sun, 11 Mar 2012 11:23:59 +0000 (11:23 +0000)]
Mention that simple commit justification applies to tb export too

7 years agoclarify text re non-tb flattened re-inclusion
Ian Jackson [Sun, 11 Mar 2012 11:21:31 +0000 (11:21 +0000)]
clarify text re non-tb flattened re-inclusion

7 years agomerge wip
Ian Jackson [Sun, 11 Mar 2012 11:07:12 +0000 (11:07 +0000)]
merge wip

7 years agomerge tip contents done
Ian Jackson [Sun, 11 Mar 2012 11:06:04 +0000 (11:06 +0000)]
merge tip contents done

7 years agomerge tip contentss: clarify arbitrariness of D
Ian Jackson [Sun, 11 Mar 2012 11:05:24 +0000 (11:05 +0000)]
merge tip contentss: clarify arbitrariness of D

7 years agocapitalise a few names
Ian Jackson [Sun, 11 Mar 2012 11:04:59 +0000 (11:04 +0000)]
capitalise a few names

7 years agomerge remove redundant element in condition
Ian Jackson [Sun, 11 Mar 2012 10:32:28 +0000 (10:32 +0000)]
merge remove redundant element in condition

7 years agowip merge tip contents
Ian Jackson [Sun, 11 Mar 2012 09:02:57 +0000 (09:02 +0000)]
wip merge tip contents

7 years agosome alternative formulations of \merge
Ian Jackson [Sun, 11 Mar 2012 08:58:18 +0000 (08:58 +0000)]
some alternative formulations of \merge

7 years agoadd definition of \nequiv. \not\equiv still does not work for some reason
Ian Jackson [Sun, 11 Mar 2012 08:57:55 +0000 (08:57 +0000)]
add definition of \nequiv.  \not\equiv still does not work for some reason

7 years agowip merge tip contents
Ian Jackson [Sun, 11 Mar 2012 08:32:59 +0000 (08:32 +0000)]
wip merge tip contents

7 years agowip merge tip contents
Ian Jackson [Sun, 11 Mar 2012 08:17:50 +0000 (08:17 +0000)]
wip merge tip contents

7 years agowip merge tip contents
Ian Jackson [Sun, 11 Mar 2012 08:12:49 +0000 (08:12 +0000)]
wip merge tip contents

7 years agowip merge tip contents
Ian Jackson [Thu, 8 Mar 2012 18:46:34 +0000 (18:46 +0000)]
wip merge tip contents

7 years agowip merge tip contents
Ian Jackson [Thu, 8 Mar 2012 18:35:43 +0000 (18:35 +0000)]
wip merge tip contents

7 years agomerge base acyclic (and condition)
Ian Jackson [Thu, 8 Mar 2012 18:35:32 +0000 (18:35 +0000)]
merge base acyclic (and condition)

7 years agoclarify P sets none overlap
Ian Jackson [Thu, 8 Mar 2012 18:35:07 +0000 (18:35 +0000)]
clarify P sets none overlap

7 years agowip merge tip contents
Ian Jackson [Thu, 8 Mar 2012 17:27:25 +0000 (17:27 +0000)]
wip merge tip contents

7 years agorename exclusive tip contents corollary
Ian Jackson [Thu, 8 Mar 2012 17:27:16 +0000 (17:27 +0000)]
rename exclusive tip contents corollary

7 years agomerge complex done
Ian Jackson [Thu, 8 Mar 2012 17:06:18 +0000 (17:06 +0000)]
merge complex done

7 years agowip merge complex - reformulate merge ends conditions
Ian Jackson [Thu, 8 Mar 2012 17:05:09 +0000 (17:05 +0000)]
wip merge complex - reformulate merge ends conditions

7 years agomerge ends condition - change condition to one that is equivalent but looks stronger...
Ian Jackson [Thu, 8 Mar 2012 16:56:57 +0000 (16:56 +0000)]
merge ends condition - change condition to one that is equivalent but looks stronger and is easier to compute

7 years agowip merge complex - final case?
Ian Jackson [Thu, 8 Mar 2012 16:50:41 +0000 (16:50 +0000)]
wip merge complex - final case?

7 years agowip merge complex - fix bug, improve merge ends condition
Ian Jackson [Thu, 8 Mar 2012 16:40:16 +0000 (16:40 +0000)]
wip merge complex - fix bug, improve merge ends condition

7 years agowip merge complex - a bug
Ian Jackson [Thu, 8 Mar 2012 16:21:33 +0000 (16:21 +0000)]
wip merge complex - a bug

7 years agowip merge complex
Ian Jackson [Thu, 8 Mar 2012 16:21:23 +0000 (16:21 +0000)]
wip merge complex

7 years agoimprove merge ends formatting
Ian Jackson [Thu, 8 Mar 2012 16:20:50 +0000 (16:20 +0000)]
improve merge ends formatting

7 years agowip merge complex - C = D
Ian Jackson [Thu, 8 Mar 2012 15:25:27 +0000 (15:25 +0000)]
wip merge complex - C = D

7 years agowip merge complex - a fix
Ian Jackson [Thu, 8 Mar 2012 15:24:45 +0000 (15:24 +0000)]
wip merge complex - a fix

7 years agowip merge complex
Ian Jackson [Tue, 6 Mar 2012 21:16:55 +0000 (21:16 +0000)]
wip merge complex

7 years agowip merge complex
Ian Jackson [Tue, 6 Mar 2012 17:47:49 +0000 (17:47 +0000)]
wip merge complex

7 years agouse \p rather than just P
Ian Jackson [Tue, 6 Mar 2012 17:46:30 +0000 (17:46 +0000)]
use \p rather than just P

7 years agowip merge complex
Ian Jackson [Tue, 6 Mar 2012 17:31:13 +0000 (17:31 +0000)]
wip merge complex

7 years agomove merge X and Y def up
Ian Jackson [Tue, 6 Mar 2012 17:29:22 +0000 (17:29 +0000)]
move merge X and Y def up

7 years agotiny clarification
Ian Jackson [Tue, 6 Mar 2012 17:17:07 +0000 (17:17 +0000)]
tiny clarification

7 years agointroduce \proofstarts
Ian Jackson [Tue, 6 Mar 2012 17:16:58 +0000 (17:16 +0000)]
introduce \proofstarts

7 years agowip merge content
Ian Jackson [Tue, 6 Mar 2012 17:11:17 +0000 (17:11 +0000)]
wip merge content

7 years agoadd some xxx's
Ian Jackson [Tue, 6 Mar 2012 14:41:54 +0000 (14:41 +0000)]
add some xxx's

7 years agoanticommit desired contents
Ian Jackson [Tue, 6 Mar 2012 14:34:10 +0000 (14:34 +0000)]
anticommit desired contents

7 years agoRename \merge to \mergeof so we can have \merge
Ian Jackson [Tue, 6 Mar 2012 14:33:33 +0000 (14:33 +0000)]
Rename \merge to \mergeof so we can have \merge

7 years agoprovide \nge and \nle (which \not uses)
Ian Jackson [Tue, 6 Mar 2012 14:32:52 +0000 (14:32 +0000)]
provide \nge and \nle (which \not uses)

7 years agowip anticommit desired contents
Ian Jackson [Tue, 6 Mar 2012 09:39:12 +0000 (09:39 +0000)]
wip anticommit desired contents

7 years agoformatting fix
Ian Jackson [Mon, 5 Mar 2012 21:22:05 +0000 (21:22 +0000)]
formatting fix

7 years agofix title etc. in merge use of no replay
Ian Jackson [Mon, 5 Mar 2012 19:51:39 +0000 (19:51 +0000)]
fix title etc. in merge use of no replay

7 years agowip anticommit
Ian Jackson [Mon, 5 Mar 2012 19:51:09 +0000 (19:51 +0000)]
wip anticommit

7 years agoimprove "no replay for merge results" (correct conditions, remove some duplicate...
Ian Jackson [Mon, 5 Mar 2012 19:50:46 +0000 (19:50 +0000)]
improve "no replay for merge results" (correct conditions, remove some duplicate stuff in proof

7 years agoprovide \base and \patch
Ian Jackson [Mon, 5 Mar 2012 19:50:03 +0000 (19:50 +0000)]
provide \base and \patch

7 years agoNo Replay for Merge Results
Ian Jackson [Mon, 5 Mar 2012 19:20:05 +0000 (19:20 +0000)]
No Replay for Merge Results

7 years agowip anticommit; use \merge
Ian Jackson [Mon, 5 Mar 2012 19:16:05 +0000 (19:16 +0000)]
wip anticommit; use \merge

7 years agodefine \merge and add it to notation section
Ian Jackson [Mon, 5 Mar 2012 19:02:45 +0000 (19:02 +0000)]
define \merge and add it to notation section

7 years agowip experiment merge
Ian Jackson [Mon, 5 Mar 2012 18:45:14 +0000 (18:45 +0000)]
wip experiment merge

7 years agowip anticommit
Ian Jackson [Mon, 5 Mar 2012 18:27:53 +0000 (18:27 +0000)]
wip anticommit

7 years agofinish merge unique base (we think)
Ian Jackson [Mon, 5 Mar 2012 18:07:15 +0000 (18:07 +0000)]
finish merge unique base (we think)

7 years agowip merge
Ian Jackson [Mon, 5 Mar 2012 17:50:03 +0000 (17:50 +0000)]
wip merge

7 years agowip merge
Ian Jackson [Mon, 5 Mar 2012 16:55:36 +0000 (16:55 +0000)]
wip merge

7 years agoheading for other side
Ian Jackson [Sun, 4 Mar 2012 20:55:43 +0000 (20:55 +0000)]
heading for other side

7 years agofix a typo
Ian Jackson [Sun, 4 Mar 2012 20:55:20 +0000 (20:55 +0000)]
fix a typo

7 years agoa possible bug
Ian Jackson [Sun, 4 Mar 2012 20:54:59 +0000 (20:54 +0000)]
a possible bug

7 years agoincrease \errorcontextlines
Ian Jackson [Sun, 4 Mar 2012 18:22:02 +0000 (18:22 +0000)]
increase \errorcontextlines

7 years agoadd some missing { } around macro args
Ian Jackson [Sun, 4 Mar 2012 18:17:41 +0000 (18:17 +0000)]
add some missing { } around macro args

7 years agosubsubsection hyperref font problems: try exciting fix (hide font info) from mdw
Ian Jackson [Sun, 4 Mar 2012 18:02:47 +0000 (18:02 +0000)]
subsubsection hyperref font problems: try exciting fix (hide font info) from mdw

7 years agodemo problem test case
Ian Jackson [Sat, 3 Mar 2012 21:02:19 +0000 (21:02 +0000)]
demo problem test case

7 years agoadd FIXME because \py seems to cause barf in \subsubsection
Ian Jackson [Sat, 3 Mar 2012 20:42:18 +0000 (20:42 +0000)]
add FIXME because \py seems to cause barf in \subsubsection

7 years agowip merge unique base
Ian Jackson [Fri, 2 Mar 2012 19:44:05 +0000 (19:44 +0000)]
wip merge unique base

7 years agowip merge unique base
Ian Jackson [Fri, 2 Mar 2012 19:07:09 +0000 (19:07 +0000)]
wip merge unique base

7 years agolemma calculation of ends, no proof yet
Ian Jackson [Fri, 2 Mar 2012 19:06:09 +0000 (19:06 +0000)]
lemma calculation of ends, no proof yet

7 years agoclarify by swapping two vars
Ian Jackson [Fri, 2 Mar 2012 19:05:45 +0000 (19:05 +0000)]
clarify by swapping two vars

7 years agoLargeexists
Ian Jackson [Fri, 2 Mar 2012 19:05:32 +0000 (19:05 +0000)]
Largeexists

7 years agomerge no replay
Ian Jackson [Fri, 2 Mar 2012 17:51:09 +0000 (17:51 +0000)]
merge no replay

7 years agowip merge
Ian Jackson [Fri, 2 Mar 2012 16:34:20 +0000 (16:34 +0000)]
wip merge

7 years agowip merge before rejoin tip merge condition
Ian Jackson [Fri, 2 Mar 2012 16:24:58 +0000 (16:24 +0000)]
wip merge before rejoin tip merge condition

7 years agowip merge
Ian Jackson [Fri, 2 Mar 2012 16:13:23 +0000 (16:13 +0000)]
wip merge

7 years agomacros \true and \false
Ian Jackson [Fri, 2 Mar 2012 16:13:19 +0000 (16:13 +0000)]
macros \true and \false

7 years agoremove symbol test section
Ian Jackson [Thu, 1 Mar 2012 14:33:02 +0000 (14:33 +0000)]
remove symbol test section

7 years ago.gitignore
Ian Jackson [Thu, 1 Mar 2012 14:32:46 +0000 (14:32 +0000)]
.gitignore

7 years agosimple commits
Ian Jackson [Thu, 1 Mar 2012 14:32:37 +0000 (14:32 +0000)]
simple commits

7 years agoa wrapper for gather
Ian Jackson [Thu, 1 Mar 2012 13:58:57 +0000 (13:58 +0000)]
a wrapper for gather

7 years agowip
Ian Jackson [Thu, 1 Mar 2012 13:49:48 +0000 (13:49 +0000)]
wip

7 years agofix up default target
Ian Jackson [Thu, 1 Mar 2012 03:45:09 +0000 (03:45 +0000)]
fix up default target

7 years agomake postscript
Ian Jackson [Thu, 1 Mar 2012 03:44:54 +0000 (03:44 +0000)]
make postscript

7 years agomakefile etc.
Ian Jackson [Thu, 1 Mar 2012 03:44:20 +0000 (03:44 +0000)]
makefile etc.

7 years agotrivial test document
Ian Jackson [Thu, 1 Mar 2012 03:43:36 +0000 (03:43 +0000)]
trivial test document

7 years agofixes
Ian Jackson [Thu, 1 Mar 2012 03:42:01 +0000 (03:42 +0000)]
fixes

7 years agoends, work, etc.
Ian Jackson [Thu, 1 Mar 2012 03:22:24 +0000 (03:22 +0000)]
ends, work, etc.

7 years agomore lemmas
Ian Jackson [Thu, 1 Mar 2012 02:39:20 +0000 (02:39 +0000)]
more lemmas

7 years agowork
Ian Jackson [Thu, 1 Mar 2012 01:57:03 +0000 (01:57 +0000)]
work

7 years agomdw's bigforall
Ian Jackson [Thu, 1 Mar 2012 01:56:59 +0000 (01:56 +0000)]
mdw's bigforall

7 years agomore style
Ian Jackson [Thu, 1 Mar 2012 01:39:24 +0000 (01:39 +0000)]
more style

7 years agohaspatch
Ian Jackson [Thu, 1 Mar 2012 01:37:48 +0000 (01:37 +0000)]
haspatch

7 years agono gather
Ian Jackson [Thu, 1 Mar 2012 01:10:09 +0000 (01:10 +0000)]
no gather

7 years agotry gather
Ian Jackson [Thu, 1 Mar 2012 01:07:24 +0000 (01:07 +0000)]
try gather

7 years agoconvert unique base to equation display
Ian Jackson [Thu, 1 Mar 2012 01:02:17 +0000 (01:02 +0000)]
convert unique base to equation display

7 years agopatchof
Ian Jackson [Thu, 1 Mar 2012 00:59:36 +0000 (00:59 +0000)]
patchof

7 years agoremove some obsolete deps
Ian Jackson [Thu, 1 Mar 2012 00:54:03 +0000 (00:54 +0000)]
remove some obsolete deps

7 years agobetter nothaspatch
Ian Jackson [Thu, 1 Mar 2012 00:53:38 +0000 (00:53 +0000)]
better nothaspatch