clasohm [Tue, 30 May 1995 11:28:13 +0200] rev 1136
fixed bug in thms_containing; changed error/warning messages;
added thms_resolving_with
clasohm [Tue, 30 May 1995 11:02:50 +0200] rev 1135
fixed bug: ThySynFun really shouldn't be deleted
clasohm [Mon, 29 May 1995 15:04:27 +0200] rev 1134
changed error message in thms_containing
clasohm [Mon, 29 May 1995 14:12:48 +0200] rev 1133
replaced "All" by "all" in ThmdbFUN's ignore parameter
clasohm [Mon, 29 May 1995 13:55:06 +0200] rev 1132
added theorem database which contains axioms and theorems indexed by the
constants they contain
nipkow [Sun, 28 May 1995 17:18:06 +0200] rev 1131
Added Church-Rosser
nipkow [Sun, 28 May 1995 17:17:43 +0200] rev 1130
Added trancl_cs
nipkow [Sat, 27 May 1995 16:10:10 +0200] rev 1129
Moved Relation from Integ to main HOL.
nipkow [Fri, 26 May 1995 18:11:47 +0200] rev 1128
Trancl is now based on Relation which used to be in Integ.
wenzelm [Fri, 26 May 1995 11:20:08 +0200] rev 1127
changed macro expander such that patterns also match prefixes of appls;
nipkow [Mon, 22 May 1995 16:00:26 +0200] rev 1126
Moved comment from ParRed.thy to ROOT.ML
nipkow [Mon, 22 May 1995 15:58:57 +0200] rev 1125
Added Park induction to Lfp.
Added Lambda to Makefile.
nipkow [Mon, 22 May 1995 14:12:40 +0200] rev 1124
Polished the presentation making it completely definitional.
lcp [Thu, 18 May 1995 11:51:23 +0200] rev 1123
Krzysztof Grabczewski's (nearly) complete AC proofs
nipkow [Mon, 15 May 1995 09:35:07 +0200] rev 1122
renamed trans_rtrancl to rtrancl_trans and modified it by expanding trans.
nipkow [Sat, 13 May 1995 14:08:24 +0200] rev 1121
Added some lemmas about r^*.
nipkow [Sat, 13 May 1995 13:46:48 +0200] rev 1120
Lambda calculus in de Bruijn notation.
Proof of confluence.
lcp [Thu, 11 May 1995 10:42:19 +0200] rev 1119
Indexing of COMP
lcp [Thu, 11 May 1995 10:38:30 +0200] rev 1118
Indexing of FILTER and COND
lcp [Thu, 11 May 1995 10:33:07 +0200] rev 1117
show_sorts
nipkow [Wed, 10 May 1995 08:38:52 +0200] rev 1116
Modified translation for pattern abstraction.
nipkow [Tue, 09 May 1995 22:10:48 +0200] rev 1115
Moved induct2 from Hoare to Lfp.
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'.