chiark / gitweb /
topbloke-formulae.git
7 years agorename merge Ordering of L... to Ordering of Ingredients
Ian Jackson [Mon, 12 Mar 2012 13:56:55 +0000 (13:56 +0000)]
rename merge Ordering of L... to Ordering of Ingredients

7 years agocreate base foreign contents
Ian Jackson [Mon, 12 Mar 2012 13:40:27 +0000 (13:40 +0000)]
create base foreign contents

7 years agochange Not Applicable [] to Not Applicable
Ian Jackson [Mon, 12 Mar 2012 13:40:19 +0000 (13:40 +0000)]
change Not Applicable [] to Not Applicable

7 years agocreate base foreign inclusion
Ian Jackson [Mon, 12 Mar 2012 13:39:14 +0000 (13:39 +0000)]
create base foreign inclusion

7 years agowip create base
Ian Jackson [Mon, 12 Mar 2012 08:55:53 +0000 (08:55 +0000)]
wip create base

7 years agocreate base coherence fix title
Ian Jackson [Sun, 11 Mar 2012 17:56:49 +0000 (17:56 +0000)]
create base coherence fix title

7 years agocreate base fix def
Ian Jackson [Sun, 11 Mar 2012 17:56:28 +0000 (17:56 +0000)]
create base fix def

7 years agoprove and use totally foreign contents
Ian Jackson [Sun, 11 Mar 2012 17:43:32 +0000 (17:43 +0000)]
prove and use totally foreign contents

7 years agofix some headings
Ian Jackson [Sun, 11 Mar 2012 17:36:15 +0000 (17:36 +0000)]
fix some headings

7 years agoformalise foreign merges
Ian Jackson [Sun, 11 Mar 2012 17:35:27 +0000 (17:35 +0000)]
formalise foreign merges

7 years agoForeign Contents section in a couple of places
Ian Jackson [Sun, 11 Mar 2012 17:35:13 +0000 (17:35 +0000)]
Foreign Contents section in a couple of places

7 years agonew foreign contents restriction
Ian Jackson [Sun, 11 Mar 2012 17:34:15 +0000 (17:34 +0000)]
new foreign contents restriction

7 years agofix a section => subsection
Ian Jackson [Sun, 11 Mar 2012 16:31:18 +0000 (16:31 +0000)]
fix a section => subsection

7 years agofix create tip tbd
Ian Jackson [Sun, 11 Mar 2012 16:31:09 +0000 (16:31 +0000)]
fix create tip tbd

7 years agowip create base
Ian Jackson [Sun, 11 Mar 2012 16:30:59 +0000 (16:30 +0000)]
wip create base

7 years agomerge conditions into conditions
Ian Jackson [Sun, 11 Mar 2012 16:09:36 +0000 (16:09 +0000)]
merge conditions into conditions

7 years agoanticommit clarify note re ingredient order
Ian Jackson [Sun, 11 Mar 2012 16:09:27 +0000 (16:09 +0000)]
anticommit clarify note re ingredient order

7 years agoanticommit conditions into conditions
Ian Jackson [Sun, 11 Mar 2012 16:09:14 +0000 (16:09 +0000)]
anticommit conditions into conditions

7 years agowip creates
Ian Jackson [Sun, 11 Mar 2012 15:57:25 +0000 (15:57 +0000)]
wip creates

7 years agoformatting move/add some qeds
Ian Jackson [Sun, 11 Mar 2012 15:56:43 +0000 (15:56 +0000)]
formatting move/add some qeds

7 years agosimple commit unique base clarification
Ian Jackson [Sun, 11 Mar 2012 15:52:47 +0000 (15:52 +0000)]
simple commit unique base clarification

7 years agoannotation calculation
Ian Jackson [Sun, 11 Mar 2012 15:51:52 +0000 (15:51 +0000)]
annotation calculation

7 years agofix up some lemmas re ends
Ian Jackson [Sun, 11 Mar 2012 14:21:01 +0000 (14:21 +0000)]
fix up some lemmas re ends

7 years agoa todo item
Ian Jackson [Sun, 11 Mar 2012 14:07:39 +0000 (14:07 +0000)]
a todo item

7 years agoanticommit foreign inclusion
Ian Jackson [Sun, 11 Mar 2012 14:05:33 +0000 (14:05 +0000)]
anticommit foreign inclusion

7 years agoa todo item
Ian Jackson [Sun, 11 Mar 2012 13:10:57 +0000 (13:10 +0000)]
a todo item

7 years agowip anticommit foreign inclusion
Ian Jackson [Sun, 11 Mar 2012 12:44:56 +0000 (12:44 +0000)]
wip anticommit foreign inclusion

7 years agomerge reference to no replay fix ref to be more regular
Ian Jackson [Sun, 11 Mar 2012 12:35:23 +0000 (12:35 +0000)]
merge reference to no replay fix ref to be more regular

7 years agoanticommit make note re merge base vs merge rhs ordering
Ian Jackson [Sun, 11 Mar 2012 12:34:59 +0000 (12:34 +0000)]
anticommit make note re merge base vs merge rhs ordering

7 years agoanticommit - split out ordering
Ian Jackson [Sun, 11 Mar 2012 12:31:53 +0000 (12:31 +0000)]
anticommit - split out ordering

7 years agomerge coherence use two implies in statement since equiv cannot represent haspatch...
Ian Jackson [Sun, 11 Mar 2012 12:24:03 +0000 (12:24 +0000)]
merge coherence use two implies in statement since equiv cannot represent haspatch and nothaspatch

7 years agoanticommit coherence
Ian Jackson [Sun, 11 Mar 2012 12:23:37 +0000 (12:23 +0000)]
anticommit coherence

7 years agoanticommit rename From Base to Into Base
Ian Jackson [Sun, 11 Mar 2012 12:08:10 +0000 (12:08 +0000)]
anticommit rename From Base to Into Base

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