nipkow [Tue, 09 May 1995 22:10:08 +0200] rev 1114
Prod is now a parent of Lfp.
Added thm induct2 to Lfp.
Changed the way patterns in abstractions are pretty printed.
It has become simpler now but fails if split has more than one argument
because then the ast-translation does not match.
clasohm [Tue, 09 May 1995 10:43:19 +0200] rev 1113
converted HOL.tex to CHOL.tex; replaced HOL.tex by CHOL.tex
clasohm [Tue, 09 May 1995 10:42:23 +0200] rev 1112
added \CHOL
lcp [Thu, 04 May 1995 14:57:06 +0200] rev 1111
Calls 'rail' program for syntax diagrams
lcp [Thu, 04 May 1995 02:02:54 +0200] rev 1110
Changed some definitions and proofs to use pattern-matching.
lcp [Thu, 04 May 1995 02:02:18 +0200] rev 1109
Changed to use split instead of fsplit. The weakening of fsplitE appears not
to affect existing proofs.
lcp [Thu, 04 May 1995 02:01:49 +0200] rev 1108
case is defined using pattern-matching
lcp [Thu, 04 May 1995 02:01:24 +0200] rev 1107
Modified proofs for new form of 'split'.
lcp [Thu, 04 May 1995 02:00:38 +0200] rev 1106
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)).
lcp [Wed, 03 May 1995 17:38:27 +0200] rev 1105
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.
lcp [Wed, 03 May 1995 17:30:36 +0200] rev 1104
Changed to use split instead of fsplit. The weakening of fsplitE appears not
to affect existing proofs.
lcp [Wed, 03 May 1995 17:22:18 +0200] rev 1103
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.
lcp [Wed, 03 May 1995 16:46:17 +0200] rev 1102
show_sorts:=true forces display of types
lcp [Wed, 03 May 1995 16:30:39 +0200] rev 1101
trivial rewording
lcp [Wed, 03 May 1995 16:10:41 +0200] rev 1100
trivial change
lcp [Wed, 03 May 1995 15:33:40 +0200] rev 1099
Covers wrapper tacticals: setwrapper, ..., addss
clasohm [Wed, 03 May 1995 15:25:30 +0200] rev 1098
fixed bug in thy_unchanged that occurred when the .thy file was changed
but the .ML file hadn't been read before;
tmpfile is now deleted immediatly after reading the .thy file in use_thy
lcp [Wed, 03 May 1995 15:06:41 +0200] rev 1097
Changed definitions so that qsplit is now defined in terms of
qfst, qsnd. AT PRESENT THERE IS NO PATTERN-MATCHING FOR QSPLIT.
lcp [Wed, 03 May 1995 14:54:43 +0200] rev 1096
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.
lcp [Wed, 03 May 1995 14:41:36 +0200] rev 1095
Changed some definitions and proofs to use pattern-matching.
lcp [Wed, 03 May 1995 14:27:51 +0200] rev 1094
Patterns can now be let-bound
lcp [Wed, 03 May 1995 14:17:01 +0200] rev 1093
Changed to use split instead of fsplit. The weakening of fsplitE appears not
to affect existing proofs.
lcp [Wed, 03 May 1995 14:03:19 +0200] rev 1092
Changed some definitions and proofs to use pattern-matching.
lcp [Wed, 03 May 1995 13:55:05 +0200] rev 1091
Changed some definitions and proofs to use pattern-matching.
lcp [Wed, 03 May 1995 13:47:24 +0200] rev 1090
Changed some definitions and proofs to use pattern-matching.
lcp [Wed, 03 May 1995 13:40:19 +0200] rev 1089
Now show_sorts:=true causes printing of types
lcp [Wed, 03 May 1995 13:35:09 +0200] rev 1088
Imported meta_eq_to_obj_eq from HOL for use with 'split'.
clasohm [Wed, 03 May 1995 12:22:17 +0200] rev 1087
replaced store_thm by bind_thm