lcp [Thu, 08 Sep 1994 12:55:50 +0200] rev 591
ZF/add_ind_def/add_fp_def_i: now prints the fixedpoint defs at the terminal
lcp [Thu, 08 Sep 1994 11:05:06 +0200] rev 590
{HOL,ZF}/indrule/quant_induct: replaced ssubst in eresolve_tac by
separate call to hyp_subst_tac. This avoids substituting in x=f(x)
{HOL,ZF}/indrule/ind_tac: now tries resolve_tac [refl]. This handles
trivial equalities such as x=a.
{HOL,ZF}/intr_elim/intro_tacsf_tac: now calls assume_tac last, to try refl
before any equality assumptions
lcp [Wed, 07 Sep 1994 17:28:53 +0200] rev 589
addition of ZF/ex/twos_compl.thy
clasohm [Wed, 07 Sep 1994 13:04:28 +0200] rev 588
moved from Contrib
clasohm [Wed, 07 Sep 1994 10:43:30 +0200] rev 587
renamed temporary variable 'base' to 'thy' in mk_structure
clasohm [Tue, 06 Sep 1994 14:44:10 +0200] rev 586
renamed base_on into mk_base and moved it to the beginning of the generated
.thy.ML file to make sure that all base theories are present when ML executes
the rest of this file
lcp [Tue, 06 Sep 1994 13:46:53 +0200] rev 585
Pure/type/unvarifyT: moved there from logic.ML
lcp [Tue, 06 Sep 1994 13:28:56 +0200] rev 584
documentation of theory sections (co)inductive and (co)datatype
wenzelm [Tue, 06 Sep 1994 13:10:38 +0200] rev 583
minor internal changes;
wenzelm [Tue, 06 Sep 1994 13:09:58 +0200] rev 582
added ext_tsig_types;
various minor changes;