chiark / gitweb /
Ian Jackson [Sun, 11 Mar 2012 11:06:04 +0000 (11:06 +0000)]
merge tip contents done
Ian Jackson [Sun, 11 Mar 2012 11:05:24 +0000 (11:05 +0000)]
merge tip contentss: clarify arbitrariness of D
Ian Jackson [Sun, 11 Mar 2012 11:04:59 +0000 (11:04 +0000)]
capitalise a few names
Ian Jackson [Sun, 11 Mar 2012 10:32:28 +0000 (10:32 +0000)]
merge remove redundant element in condition
Ian Jackson [Sun, 11 Mar 2012 09:02:57 +0000 (09:02 +0000)]
wip merge tip contents
Ian Jackson [Sun, 11 Mar 2012 08:58:18 +0000 (08:58 +0000)]
some alternative formulations of \merge
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
Ian Jackson [Sun, 11 Mar 2012 08:32:59 +0000 (08:32 +0000)]
wip merge tip contents
Ian Jackson [Sun, 11 Mar 2012 08:17:50 +0000 (08:17 +0000)]
wip merge tip contents
Ian Jackson [Sun, 11 Mar 2012 08:12:49 +0000 (08:12 +0000)]
wip merge tip contents
Ian Jackson [Thu, 8 Mar 2012 18:46:34 +0000 (18:46 +0000)]
wip merge tip contents
Ian Jackson [Thu, 8 Mar 2012 18:35:43 +0000 (18:35 +0000)]
wip merge tip contents
Ian Jackson [Thu, 8 Mar 2012 18:35:32 +0000 (18:35 +0000)]
merge base acyclic (and condition)
Ian Jackson [Thu, 8 Mar 2012 18:35:07 +0000 (18:35 +0000)]
clarify P sets none overlap
Ian Jackson [Thu, 8 Mar 2012 17:27:25 +0000 (17:27 +0000)]
wip merge tip contents
Ian Jackson [Thu, 8 Mar 2012 17:27:16 +0000 (17:27 +0000)]
rename exclusive tip contents corollary
Ian Jackson [Thu, 8 Mar 2012 17:06:18 +0000 (17:06 +0000)]
merge complex done
Ian Jackson [Thu, 8 Mar 2012 17:05:09 +0000 (17:05 +0000)]
wip merge complex - reformulate merge ends conditions
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
Ian Jackson [Thu, 8 Mar 2012 16:50:41 +0000 (16:50 +0000)]
wip merge complex - final case?
Ian Jackson [Thu, 8 Mar 2012 16:40:16 +0000 (16:40 +0000)]
wip merge complex - fix bug, improve merge ends condition
Ian Jackson [Thu, 8 Mar 2012 16:21:33 +0000 (16:21 +0000)]
wip merge complex - a bug
Ian Jackson [Thu, 8 Mar 2012 16:21:23 +0000 (16:21 +0000)]
wip merge complex
Ian Jackson [Thu, 8 Mar 2012 16:20:50 +0000 (16:20 +0000)]
improve merge ends formatting
Ian Jackson [Thu, 8 Mar 2012 15:25:27 +0000 (15:25 +0000)]
wip merge complex - C = D
Ian Jackson [Thu, 8 Mar 2012 15:24:45 +0000 (15:24 +0000)]
wip merge complex - a fix
Ian Jackson [Tue, 6 Mar 2012 21:16:55 +0000 (21:16 +0000)]
wip merge complex
Ian Jackson [Tue, 6 Mar 2012 17:47:49 +0000 (17:47 +0000)]
wip merge complex
Ian Jackson [Tue, 6 Mar 2012 17:46:30 +0000 (17:46 +0000)]
use \p rather than just P
Ian Jackson [Tue, 6 Mar 2012 17:31:13 +0000 (17:31 +0000)]
wip merge complex
Ian Jackson [Tue, 6 Mar 2012 17:29:22 +0000 (17:29 +0000)]
move merge X and Y def up
Ian Jackson [Tue, 6 Mar 2012 17:17:07 +0000 (17:17 +0000)]
tiny clarification
Ian Jackson [Tue, 6 Mar 2012 17:16:58 +0000 (17:16 +0000)]
introduce \proofstarts
Ian Jackson [Tue, 6 Mar 2012 17:11:17 +0000 (17:11 +0000)]
wip merge content
Ian Jackson [Tue, 6 Mar 2012 14:41:54 +0000 (14:41 +0000)]
add some xxx's
Ian Jackson [Tue, 6 Mar 2012 14:34:10 +0000 (14:34 +0000)]
anticommit desired contents
Ian Jackson [Tue, 6 Mar 2012 14:33:33 +0000 (14:33 +0000)]
Rename \merge to \mergeof so we can have \merge
Ian Jackson [Tue, 6 Mar 2012 14:32:52 +0000 (14:32 +0000)]
provide \nge and \nle (which \not uses)
Ian Jackson [Tue, 6 Mar 2012 09:39:12 +0000 (09:39 +0000)]
wip anticommit desired contents
Ian Jackson [Mon, 5 Mar 2012 21:22:05 +0000 (21:22 +0000)]
formatting fix
Ian Jackson [Mon, 5 Mar 2012 19:51:39 +0000 (19:51 +0000)]
fix title etc. in merge use of no replay
Ian Jackson [Mon, 5 Mar 2012 19:51:09 +0000 (19:51 +0000)]
wip anticommit
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
Ian Jackson [Mon, 5 Mar 2012 19:50:03 +0000 (19:50 +0000)]
provide \base and \patch
Ian Jackson [Mon, 5 Mar 2012 19:20:05 +0000 (19:20 +0000)]
No Replay for Merge Results
Ian Jackson [Mon, 5 Mar 2012 19:16:05 +0000 (19:16 +0000)]
wip anticommit; use \merge
Ian Jackson [Mon, 5 Mar 2012 19:02:45 +0000 (19:02 +0000)]
define \merge and add it to notation section
Ian Jackson [Mon, 5 Mar 2012 18:45:14 +0000 (18:45 +0000)]
wip experiment merge
Ian Jackson [Mon, 5 Mar 2012 18:27:53 +0000 (18:27 +0000)]
wip anticommit
Ian Jackson [Mon, 5 Mar 2012 18:07:15 +0000 (18:07 +0000)]
finish merge unique base (we think)
Ian Jackson [Mon, 5 Mar 2012 17:50:03 +0000 (17:50 +0000)]
wip merge
Ian Jackson [Mon, 5 Mar 2012 16:55:36 +0000 (16:55 +0000)]
wip merge
Ian Jackson [Sun, 4 Mar 2012 20:55:43 +0000 (20:55 +0000)]
heading for other side
Ian Jackson [Sun, 4 Mar 2012 20:55:20 +0000 (20:55 +0000)]
fix a typo
Ian Jackson [Sun, 4 Mar 2012 20:54:59 +0000 (20:54 +0000)]
a possible bug
Ian Jackson [Sun, 4 Mar 2012 18:22:02 +0000 (18:22 +0000)]
increase \errorcontextlines
Ian Jackson [Sun, 4 Mar 2012 18:17:41 +0000 (18:17 +0000)]
add some missing { } around macro args
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
Ian Jackson [Sat, 3 Mar 2012 21:02:19 +0000 (21:02 +0000)]
demo problem test case
Ian Jackson [Sat, 3 Mar 2012 20:42:18 +0000 (20:42 +0000)]
add FIXME because \py seems to cause barf in \subsubsection
Ian Jackson [Fri, 2 Mar 2012 19:44:05 +0000 (19:44 +0000)]
wip merge unique base
Ian Jackson [Fri, 2 Mar 2012 19:07:09 +0000 (19:07 +0000)]
wip merge unique base
Ian Jackson [Fri, 2 Mar 2012 19:06:09 +0000 (19:06 +0000)]
lemma calculation of ends, no proof yet
Ian Jackson [Fri, 2 Mar 2012 19:05:45 +0000 (19:05 +0000)]
clarify by swapping two vars
Ian Jackson [Fri, 2 Mar 2012 19:05:32 +0000 (19:05 +0000)]
Largeexists
Ian Jackson [Fri, 2 Mar 2012 17:51:09 +0000 (17:51 +0000)]
merge no replay
Ian Jackson [Fri, 2 Mar 2012 16:34:20 +0000 (16:34 +0000)]
wip merge
Ian Jackson [Fri, 2 Mar 2012 16:24:58 +0000 (16:24 +0000)]
wip merge before rejoin tip merge condition
Ian Jackson [Fri, 2 Mar 2012 16:13:23 +0000 (16:13 +0000)]
wip merge
Ian Jackson [Fri, 2 Mar 2012 16:13:19 +0000 (16:13 +0000)]
macros \true and \false
Ian Jackson [Thu, 1 Mar 2012 14:33:02 +0000 (14:33 +0000)]
remove symbol test section
Ian Jackson [Thu, 1 Mar 2012 14:32:46 +0000 (14:32 +0000)]
.gitignore
Ian Jackson [Thu, 1 Mar 2012 14:32:37 +0000 (14:32 +0000)]
simple commits
Ian Jackson [Thu, 1 Mar 2012 13:58:57 +0000 (13:58 +0000)]
a wrapper for gather
Ian Jackson [Thu, 1 Mar 2012 13:49:48 +0000 (13:49 +0000)]
wip
Ian Jackson [Thu, 1 Mar 2012 03:45:09 +0000 (03:45 +0000)]
fix up default target
Ian Jackson [Thu, 1 Mar 2012 03:44:54 +0000 (03:44 +0000)]
make postscript
Ian Jackson [Thu, 1 Mar 2012 03:44:20 +0000 (03:44 +0000)]
makefile etc.
Ian Jackson [Thu, 1 Mar 2012 03:43:36 +0000 (03:43 +0000)]
trivial test document
Ian Jackson [Thu, 1 Mar 2012 03:42:01 +0000 (03:42 +0000)]
fixes
Ian Jackson [Thu, 1 Mar 2012 03:22:24 +0000 (03:22 +0000)]
ends, work, etc.
Ian Jackson [Thu, 1 Mar 2012 02:39:20 +0000 (02:39 +0000)]
more lemmas
Ian Jackson [Thu, 1 Mar 2012 01:57:03 +0000 (01:57 +0000)]
work
Ian Jackson [Thu, 1 Mar 2012 01:56:59 +0000 (01:56 +0000)]
mdw's bigforall
Ian Jackson [Thu, 1 Mar 2012 01:39:24 +0000 (01:39 +0000)]
more style
Ian Jackson [Thu, 1 Mar 2012 01:37:48 +0000 (01:37 +0000)]
haspatch
Ian Jackson [Thu, 1 Mar 2012 01:10:09 +0000 (01:10 +0000)]
no gather
Ian Jackson [Thu, 1 Mar 2012 01:07:24 +0000 (01:07 +0000)]
try gather
Ian Jackson [Thu, 1 Mar 2012 01:02:17 +0000 (01:02 +0000)]
convert unique base to equation display
Ian Jackson [Thu, 1 Mar 2012 00:59:36 +0000 (00:59 +0000)]
patchof
Ian Jackson [Thu, 1 Mar 2012 00:54:03 +0000 (00:54 +0000)]
remove some obsolete deps
Ian Jackson [Thu, 1 Mar 2012 00:53:38 +0000 (00:53 +0000)]
better nothaspatch
Ian Jackson [Thu, 1 Mar 2012 00:49:39 +0000 (00:49 +0000)]
pancs, pends
Ian Jackson [Thu, 1 Mar 2012 00:49:30 +0000 (00:49 +0000)]
amsmath
Ian Jackson [Thu, 1 Mar 2012 00:28:46 +0000 (00:28 +0000)]
try leqno
Ian Jackson [Thu, 1 Mar 2012 00:17:21 +0000 (00:17 +0000)]
full stop
Ian Jackson [Thu, 1 Mar 2012 00:14:45 +0000 (00:14 +0000)]
drop mnsymbol, use mathabx
Ian Jackson [Thu, 1 Mar 2012 00:11:46 +0000 (00:11 +0000)]
define patch
Ian Jackson [Thu, 1 Mar 2012 00:04:45 +0000 (00:04 +0000)]
nice formatting for notation
Ian Jackson [Wed, 29 Feb 2012 23:45:11 +0000 (23:45 +0000)]
displays
~ian / topbloke-formulae.git / log