summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files | gz |
help

(0) -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip

(0) -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip

converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex

added \CHOL

Calls 'rail' program for syntax diagrams

Changed some definitions and proofs to use pattern-matching.

Changed to use split instead of fsplit. The weakening of fsplitE appears not
to affect existing proofs.

case is defined using pattern-matching

Modified proofs for new form of 'split'.

Added pattern-matching code from CHOL/Prod.thy. Changed
definitions so that split is now defined in terms of fst, snd. Now split is
polymorphic. Deleted fsplit, as split(...)::o gives a similar effect -- NOT
identical though, as fsplit(P,z) implied that z was a pair, while split(P,z)
means only P(fst(z),snd(z)).

Modified proofs for (q)split, fst, snd for new
definitions. The rule f(q)splitE is now called (q)splitE and is weaker than
before. The rule '(q)split' is now a meta-equality; this required modifying
all proofs involving e.g. split RS trans.

Changed to use split instead of fsplit. The weakening of fsplitE appears not
to affect existing proofs.