lcp [Tue, 06 Jun 1995 10:33:32 +0200] rev 1143
Now string_of_vname checks for the empty variable name,
catching the exception LIST.
lcp [Fri, 02 Jun 1995 10:38:48 +0200] rev 1142
Corrected comments in headers
clasohm [Thu, 01 Jun 1995 13:25:06 +0200] rev 1141
commented thms_unifying_with out; placed thm_db into signature again;
placed structures ThmDB and Readthy into Pure again;
changed init_thy_reader so that thm_db and loaded_thys are preserved
(necessary e.g. for ZF)
nipkow [Thu, 01 Jun 1995 12:31:52 +0200] rev 1140
Added dependence on Thy/thm_database.ML
mueller [Wed, 31 May 1995 10:46:46 +0200] rev 1139
*** empty log message ***
mueller [Wed, 31 May 1995 10:45:00 +0200] rev 1138
polish
clasohm [Tue, 30 May 1995 11:57:27 +0200] rev 1137
removed thm_num and thm_db from signature
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.