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

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.

prove_case_equation now calls uses meta_eq_to_obj_eq to cope
with new form of 'split'. Tried calling simp_tac instead of using resolution
with trans, but it was significantly slower: 98.3 secs instead of 91.2 secs
for ex/Enum.

show_sorts:=true forces display of types

trivial rewording