no longer forces default;

misc tuning;

removed one blank at end of line 37

refer to SOME, NONE on top-level;

adapted for 1.09.27 (and later);

open General (type option is in Option in the newer versions, but always the top-level);

adapted to SML/NJ 1.09.27; minor cleanup;

Added 'induct_tac'

Updates because nat_ind_tac no longer appends "1" to the ind.var.

removed space;

induct_tac

expandshort

Introduced a generic "induct_tac" which picks up the right induction scheme automatically. Also changed nat_ind_tac, which does no longer append a "1" to the name of the induction variable. This caused some changes...

get_thydata accesses the second component of the data field. This component used to be empty until set at the end of loading an ML file. Now the second component is already set when the thy file has ben read.

Main changes are: - Lemmas for blift and plift are deleted - added split_tac for If (via If2, as If does not begin with a constant) - added new lemmata relating TT, FF and booleans: Def_bool1, Def_bool2, Def_bool3,Def_bool4 They are added to !simpset, but should not cause difficulties - added lemma andalso_or relating | on booleans and andalso on truth values - deleted If_and_if and andalso from !simpset: Pay attention, may kill your proofs! - added adm lemmas for (f x)~=TT and (f x)~=FF.

rename_params_rule used to check if the new name clashed with a free name in the whole goal state. Now checks only the subgoal concerned.

deleted definitions for blift and plift

Complete Redesign of Theory, main points are: - Extension of the continuity prover: * Lemmas about continuity of flift1 and flift2 are generalized * Lemmas about continuity of mixed definitions of HOL and LCF terms generalized Pay attention: Sometimes proofs are shorter now! - a number of new lemmas concerning flift1, flift2, Def and Undef, Def_less_is_eq (Def x << y = (Def x = y)) and lemmas characterizing flift1 and flift2 are added to !simpset Pay attention: Sometimes proofs are shorter now! - added tactic def_tac for eliminating x~=UU in assumptions

added liftpair definition

only in comments

minor changes due to more powerful continuity check in Lift3.ML

added some comments;

Addition of printed tracing. Also some tidying

A bit of tidying

added dependencies on ax_ops/*.ML and domain/*.ML

changed priority of '%': now no parenteses needed for '[...] == %x. [...]'

moved antisym_less_inverse,box_less from Porder.ML to Porder0.ML

Added NatDef

Necessary inclusion of depth bound into blast_tac call

Ran expandshort

Unfortunately, the \\< syntax does not always accept the beginning of a line

Loop detection: before expanding a haz formula, see whether it is a duplicate and, if so, delete it. Recursion detection: transitivity and similar rules, when applied, put the new formulae at the end of a branch and not at the front (in effect).