summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files | gz |
help

(0) -300 -100 -30 -10 -6 +6 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip

(0) -300 -100 -30 -10 -6 +6 +10 +30 +100 +300 +1000 +3000 +10000 +30000 tip

Fri, 09 Sep 1994 11:45:44 +0200
Logics/HOL: Section 3, added Pow and its rule. New sections 6 on the

Logics/HOL: Section 3, added Pow and its rule. New sections 6 on the
datatype declaration and 7 on (co)inductive definitions. Added mention of
directory IMP.

ZF/Zorn/next_bounded: deleted this proof, which was already in comments

documentation on theories

ZF/add_ind_def/add_fp_def_i: now prints the fixedpoint defs at the terminal

{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

addition of ZF/ex/twos_compl.thy