nipkow [Sun, 11 Sep 1994 10:31:17 +0200] rev 141
Allowed string as function name in primrec header
lcp [Thu, 08 Sep 1994 11:01:45 +0200] rev 140
{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 13:17:34 +0200] rev 139
HOL/IMP/Equiv/bexp_iff: split proof into separate directions, to be faster
nipkow [Tue, 06 Sep 1994 16:46:27 +0200] rev 138
changed names
nipkow [Tue, 06 Sep 1994 16:15:59 +0200] rev 137
Converted rules to primrecs
lcp [Tue, 06 Sep 1994 13:24:29 +0200] rev 136
corrected comment re treatment of types such as (bool*bool)*bool
lcp [Tue, 06 Sep 1994 10:56:54 +0200] rev 135
HOL/ex/PropLog.thy: tidied
lcp [Tue, 06 Sep 1994 10:54:46 +0200] rev 134
HOL/ind_syntax/factors: now returns only factors in the product type that
associate to the right. Previously the proof of the induction rule
crashed on types such as (bool*bool)*bool.
nipkow [Wed, 31 Aug 1994 17:50:59 +0200] rev 133
Added IMP, which necessiated changes in intr_elim.tex (mk_cases).
Improved layout for set comprehension in Set.thy.
nipkow [Wed, 31 Aug 1994 16:25:19 +0200] rev 132
Renamed a few types and vars