edits.txt

tuned;

EDITS TO THE ISABELLE SYSTEM FOR 1993

11 January 

*/README: Eliminated references to Makefile.NJ, which no longer exists.

**** New tar file placed on /homes/lcp (464K) **** 

14 January

Provers/simp/pr_goal_lhs: now distinct from pr_goal_concl so that tracing
prints conditions correctly.

{CTT/arith,HOL/ex/arith/ZF/arith}/add_mult_distrib: renamed from
add_mult_dist, to agree with the other _distrib rules

20 January

Pure/Syntax/type_ext.ML: "I have fixed a few anomalies in the pretty
printing annotations for types.  Only the layout has changed." -- Toby

21 January

{CTT/arith,HOL/ex/arith/ZF/arith}/add_inverse_diff: renamed to add_diff_inverse

22 January

ZF/ex/equiv: new theory of equivalence classes
ZF/ex/integ: new theory of integers
HOL/set.thy: added indentation of 3 to all binding operators

ZF/bool/boolI0,boolI1: renamed as bool_0I, bool_1I

25 January

MAKE-ALL (NJ 0.75) ran perfectly.  It took 3:19 hours!?

ZF/bool/not,and,or,xor: new

27 January

ZF/ex/bin: new theory of binary integer arithmetic

27 January

MAKE-ALL (Poly/ML) ran perfectly.  It took 6:33 hours???
(ZF took almost 5 hours!)

**** New tar file placed on /homes/lcp (472K) **** 

HOL/set/UN_cong,INT_cong: new
HOL/subset/mem_rews,set_congs,set_ss: new
HOL/simpdata/o_apply: new; added to HOL_ss

29 January

Pure/Thy/syntax/mk_structure: the dummy theory created by type infixes is
now called name^"(type infix)" instead of "", avoid triggering a spurious
error "Attempt to merge different versions of theory: " in
Pure/sign/merge_stamps

2 February

MAKE-ALL (Poly/ML) ran perfectly.  It took 2:48 hours.  Runs in 1992 took
under 2:20 hours, but the new files in ZF/ex take time: nearly 23 minutes
according to make10836.log.

Pure/Thy/scan/comment: renamed from komt
Pure/Thy/scan/numeric: renamed from zahl

Pure/Syntax/syntax,lexicon,type_ext,extension,sextension: modified by
Tobias to change ID, TVAR, ... to lower case.

Cube/cube.thy,HOL/hol.thy,HOL/set.thy,CTT/ctt.thy,LK/lk.thy,ZF/zf.thy: now
with ID, ... in lower case and other tidying

3 February

MAKE-ALL (Poly/ML) ran perfectly.  It took 2:50 hours.

4 February

HOL/nat/nat_ss: now includes the rule Suc_less_eq: (Suc(m) < Suc(n)) = (m<n)
and the nat_case rules and congruence rules

HOL/sum/sumE: now has the "strong" form with equality assumptions.  WAS
    val prems = goalw Sum.thy [Inl_def,Inr_def]
	"[| !!x::'a. P(Inl(x));  !!y::'b. P(Inr(y)) \
    \    |] ==> P(s)";
    by (res_inst_tac [("t","s")] (Rep_Sum_inverse RS subst) 1);
    by (rtac (rewrite_rule [Sum_def] Rep_Sum RS CollectE) 1);
    by (REPEAT (eresolve_tac [disjE,exE,ssubst] 1 ORELSE resolve_tac prems 1));
    val sumE = result();

8 February

Changes from Tobias:
Pure/Thy/parse: now list_of admits the empty phrase, while listof_1 does not
Pure/Thy/syntax: uses new list_of, list_of1

9 February

HOL/ex/arith: moved to main HOL directory
HOL/prod: now define the type "unit" and constant "(): unit"

11 February

HOL/arith: eliminated redefinitions of nat_ss and arith_ss

12 February

MAKE-ALL (Poly/ML) ran perfectly.  It took 2:50 hours.

Pure/Thy/scan/string: now correctly recognizes ML-style strings.

15 February

MAKE-ALL (NJ 0.75) ran perfectly.  It took 1:37 hours (on albatross)
MAKE-ALL (NJ 0.75) ran perfectly.  It took 2:42 hours (on dunlin)
MAKE-ALL (Poly/ML) ran perfectly.  It took 2:53 hours (on dunlin)

**** New tar file placed on /homes/lcp (480K) **** 

18 February

Pure/Syntax/earley0A/compile_xgram: Tobias deleted the third argument, as
it was unused.

Pure/Syntax/earley0A: modified accordingly.

19 February

MAKE-ALL (NJ 0.75) ran perfectly.  It took 3:37 hours 
MAKE-ALL (Poly/ML) ran perfectly.  It took 2:52 hours

**** New tar file placed on /homes/lcp (480K) **** 

20 February

MAKE-ALL (NJ 0.93) ran perfectly.  It took 3:30 hours 

10 March

HOL/fun/image_eqI: fixed bad pattern

11 March

MAKE-ALL (Poly/ML) failed in HOL!

HOL/fun: moved "mono" proofs to HOL/subset, since they rely on subset laws
of Int and Un.

12 March

ZF/ex/misc: new example from Bledsoe

15 March

ZF/perm: two new theorems inspired by Pastre

16 March

Weakened congruence rules for HOL: speeds simplification considerably by
NOT simplifying the body of a conditional or eliminator.

HOL/simpdata/mk_weak_congs: new, to make weakened congruence rules

HOL/simpdata/congs: renamed HOL_congs and weakened the "if" rule

HOL/simpdata/HOL_congs: now contains polymorphic rules for the overloaded
operators < and <=

HOL/prod: weakened the congruence rule for split
HOL/sum: weakened the congruence rule for case
HOL/nat: weakened the congruence rule for nat_case and nat_rec
HOL/list: weakened the congruence rule for List_rec and list_rec

HOL & test rebuilt perfectly

Pure/goals/prepare_proof/mkresult: fixed bug in signature check.  Now
compares the FINAL signature with that from the original theory.

Pure/goals/prepare_proof: ensures that [prove_]goalw checks that the
definitions do not update the proof state.

17 March

MAKE-ALL (Poly/ML) ran perfectly.

18 March

MAKE-ALL (Poly/ML) failed in HOL/ex/Substitutions

HOL/ex/Subst/setplus: changed Set.thy to Setplus.thy where
necessary

ZF/perm: proved some rules about inj and surj

ZF/ex/misc: did some of Pastre's examples

Pure/library/gen_ins,gen_union: new

HOL/ex/Subst/subst: renamed rangeE to srangeE

18 March

MAKE-ALL (Poly/ML) failed in HOL/ex/term due to renaming of list_ss in
ex/Subst/alist

HOL/list/list_congs: new; re-organized simpsets a bit

Pure/goals/sign_error: new

Pure/goals/prepare_proof,by_com: now print the list of new theories when
the signature of the proof state changes 

HOL/prod,sexp: renamed fst, snd to fst_conv, snd_conv to avoid over-writing
the library functions fst, snd

HOL/fun/image_compose: new

21 March

MAKE-ALL (NJ 0.93) ran perfectly.  It took 3:50 hours 
MAKE-ALL (Poly/ML) ran perfectly.  It took 3:21 hours
Much slower now (about 30 minutes!) because of HOL/ex/Subst

**** New tar file placed on /homes/lcp (504K) **** 

ZF/pair,simpdata: renamed fst, snd to fst_conv, snd_conv to avoid over-writing
the library functions fst, snd

HOL/prod/prod_fun_imageI,E: new

HOL/ex/Subst/Unify: renamed to Unifier to avoid clobbering structure Unify
of Pure

24 March

HOL/trancl/comp_subset_Sigma: new
HOL/wf/wfI: new

HOL/Subst: moved from HOL/ex/Subst to shorten pathnames
HOL/Makefile: target 'test' now loads Subst/ROOT separately

*** Installation of gfp, coinduction, ... to HOL ***

HOL/gfp,llist: new
HOL/univ,sexp,list: replaced with new version

Sexp is now the set of all well-founded trees, each of type 'a node set.
There is no longer a type 'sexp'.  Initial algebras require more explicit
type checking than before.  Defining a type 'sexp' would eliminate this,
but would also require a whole new set of primitives, similar to those
defined in univ.thy but restricted to well-founded trees.

25 March

Pure/thm: renamed 'bires' to 'eres' in many places (not exported) --
biresolution now refers to resolution with (flag,rule) pairs.

Pure/thm/bicompose_aux: SOUNDNESS BUG concerning variable renaming.  A Var in
a premise was getting renamed when its occurrence in the flexflex pairs was
not.  Martin Coen supplied the following proof of True=False in HOL:

    val [prem] = goal Set.thy "EX a:{c}.p=a ==> p=c";
    br (prem RS bexE) 1; be ssubst 1; be singletonD 1;
    val l1 = result();

    val rls = [refl] RL [bexI] RL [l1];

    goal Set.thy "True = False";
    brs rls 1; br singletonI 1;
    result();

Marcus Moore noted that the error only occurred with
Logic.auto_rename:=false.  Elements of the fix:

1.  rename_bvs, rename_bvars and bicompose_aux/newAs take tpairs (the
existing flex-flex pairs) as an extra argument.  rename_bvs preserves all
Vars in tpairs.

2.  bicompose_aux/tryasms and res now unpack the "cell" and supply its tpairs
to newAs.

HOL/lfp,gfp,ex/set: renamed Tarski to lfp_Tarski

HOL/lfp,list,llist,nat,sexp,trancl,Subst/uterm,ex/simult,ex/term: renamed
def_Tarski to def_lfp_Tarski 

26 March

MAKE-ALL (NJ 0.93) ran perfectly.  It took 4:25 hours!
MAKE-ALL (Poly/ML) ran perfectly.  It took 3:54 hours! (jobs overlapped)

Pure/Thy/scan/is_digit,is_letter: deleted.  They are already in
Pure/library, and these versions used non-Standard string comparisons!

Repairing a fault reported by David Aspinall:
  show_types := true;  read "a";  (* followed by  'prin it' for NJ *)
Raises exception  LIST "hd".   Also has the side effect of leaving
show_types set at false. 

Pure/goals/read: no longer creates a null TVar
Pure/Syntax/lexicon/string_of_vname: now handles null names
Pure/Syntax/printer/string_of_typ: tidied

/usr/groups/theory/isabelle/92/Pure/thm: replaced by new version to fix bug
MAKE-ALL on this directory ran perfectly
/usr/groups/theory/ml-aftp/Isabelle92.tar.Z: replaced by new version

29 March

MAKE-ALL (NJ 0.93) ran perfectly.  It took 4:14 hours!
MAKE-ALL (Poly/ML) ran perfectly.  It took 3:43 hours!

**** New tar file placed on /homes/lcp (518K) **** 

30 March

ZF/univ/cons_in_Vfrom: deleted "[| a: Vfrom(A,i);  b<=Vfrom(A,i) |] ==>
cons(a,b) : Vfrom(A,succ(i))" since it was useless.

8 April

MAKE-ALL (Poly/ML) ran perfectly.  It took 3:49 hours!

**** New tar file placed on /homes/lcp (520K) **** 

**** Updates for pattern unification (Tobias Nipkow) ****

Pure/pattern.ML: new, pattern unification

Pure/Makefile and ROOT.ML: included pattern.ML

Pure/library.ML: added predicate downto0

Pure/unify.ML: call pattern unification first. Removed call to could_unify.

FOL/Makefile/FILES: now mentions ifol.ML (previously repeated fol.ML instead)

**** Installation of Martin Coen's FOLP (FOL + proof objects) ****

renamed PFOL, PIFOL to FOLP, IFOLP, etc.

9 April

MAKE-ALL (NJ 0.93) ran perfectly.  It took 4:05 hours!
MAKE-ALL (Poly/ML) ran perfectly.  It took 3:31 hours!

**** New tar file placed on /homes/lcp (576K) **** 

**** Installation of Discrimination Nets ****

*Affected files (those mentioning Stringtree, compat_thms or rtr_resolve_tac)
Pure/ROOT.ML,goals.ML,stringtree.ML,tactic.ML
Provers/simp.ML
HOL/ex/meson.ML

*Affected files (those mentioning compat_resolve_tac)
Pure/tactic.ML
Provers/typedsimp.ML
CTT/ctt.ML

Pure/stringtree: saved on Isabelle/old
Pure/net: new
Pure/Makefile/FILES: now mentions net.ML, not stringtree.ML
Pure/ROOT: now mentions net.ML, not stringtree.ML

Pure/goals/compat_goal: DELETED

Pure/tactic/compat_thms,rtr_resolve_tac,compat_resolve_tac,insert_thm,
delete_thm,head_string: DELETED

Pure/tactic/biresolve_from_nets_tac, bimatch_from_nets_tac,
net_biresolve_tac, net_bimatch_tac, resolve_from_net_tac, match_from_net_tac,
net_resolve_tac, net_match_tac: NEW

Pure/tactic/filt_resolve_tac: new implementation using nets!

Provers/simp: replaced by new version

Provers/typedsimp: changed compat_resolve_tac to filt_resolve_tac and
updated comments

CTT/ctt.ML: changed compat_resolve_tac to filt_resolve_tac 
ZF/simpdata/typechk_step_tac: changed compat_resolve_tac to filt_resolve_tac

CTT tested

HOL/ex/meson/ins_term,has_reps: replaced Stringtree by Net

FOL tested

Provers/simp/cong_const: new, replaces head_string call in cong_consts
Provers/simp: renamed variables: atomic to at and cong_consts to ccs

ZF/ex/bin/integ_of_bin_type: proof required reordering of rules --
typechk_tac now respects this ordering!

ZF tested

DOCUMENTATION

Logics/CTT: Removed mention of compat_resolve_tac 
Ref/goals: deleted compat_goal's entry

Provers/hypsubst/lasthyp_subst_tac: deleted

FOLP/ROOT/dest_eq: corrected; now hyp_subst_tac works!

12 April

MAKE-ALL (NJ 0.93) ran perfectly.  It took 4:03 hours!
MAKE-ALL (Poly/ML) ran perfectly.  It took 3:28 hours!

FOLP/{int-prover,classical}/safe_step_tac: uses eq_assume_tac, not assume_tac
FOLP/{int-prover,classical}/inst_step_tac: restored, calls assume and mp_tac
FOLP/{int-prover,classical}/step_tac: calls inst_step_tac 

{FOL,FOLP}/int-prover/safe_brls: removed (asm_rl,true) since assume_tac is
used explicitly!!

FOLP/ifolp/uniq_assume_tac: new, since eq_assume_tac is almost useless

FOLP/{int-prover,classical}/uniq_mp_tac: replace eq_mp_tac and call
uniq_assume_tac

Provers/classical: REPLACED BY 'NET' VERSION!

13 April

MAKE-ALL (Poly/ML) failed in ZF and ran out of quota for Cube.

Unification bug (nothing to do with pattern unification)
Cleaning of flex-flex pairs attempts to remove all occurrences of bound
variables not common to both sides.  Arguments containing "banned" bound
variables are deleted -- but this should ONLY be done if the occurrence is
rigid!

unify/CHANGE_FAIL: new, for flexible occurrence of bound variable
unify/change_bnos: now takes "flex" as argument, indicating path status

14 April

MAKE-ALL (Poly/ML) failed in HOL (ASM_SIMP_TAC redefined!) and LK

LK/ex/hard-quant/37: added "by flexflex_tac" to compensate for flexflex
changes

Pure/goals/gethyps: now calls METAHYPS directly

rm-logfiles: no longer mentions directories.  WAS
    rm log {Pure,FOL,ZF,LCF,CTT,LK,Modal,HOL,Cube}/make*.log
    rm {FOL,ZF,LCF,CTT,LK,Modal,HOL,Cube}/test
    rm {FOL,ZF,LCF,CTT,LK,Modal,HOL,Cube}/.*.thy.ML
    rm {FOL,ZF,HOL}/ex/.*.thy.ML

MAKE-ALL (Poly/ML) ran perfectly.  It took 2:39 hours! (albatross)

New version of simp on Isabelle/new -- instantiates unknowns provided only
one rule may do so [SINCE REJECTED DUE TO UNPREDICTABLE BEHAVIOR]

works with FOLP/ex/nat, but in general could fail in the event of
overlapping rewrite rules, since FOLP always instantiates unknowns during
rewriting.

ZF: tested with new version

HOL: tested with new version, appeared to loop in llist/Lmap_ident

**** NEW VERSION OF ASM_SIMP_TAC, WITH METAHYPS ****

ZF: failed in perm/comp_mem_injD1: the rule anti_refl_rew is too ambiguous!
ZF/wfrec: all uses of wf_ss' require
by (METAHYPS (fn hyps => cut_facts_tac hyps 1 THEN
                         SIMP_TAC (wf_ss' addrews (hyps)) 1) 1);

ZF/epsilon/eclose_least: changed ASM_SIMP_TAC to SIMP_TAC; this makes
METAHYPS version work

ZF/arith/add_not_less_self: adds anti_refl_rew

ZF/ex/prop-log/hyps_finite: the use of UN_I is very bad -- too undirected.
Swapping the premises of UN_I would probably allow instantiation.

ZF otherwise seems to work!

HOL/llist/llistE: loops! due to rewriting by Rep_LList_LCons of Vars

HOL/ex/prop-log/comp_lemma: failed due to uninstantiated Var in 
(CCONTR_rule RS allI)

*** REJECTED

15 April

These overnight runs involve Provers/simp.ML with old treatment of rules
(match_tac) and no METAHYPS; they test the new flexflex pairs and
discrimination nets, to see whether it runs faster.

MAKE-ALL (NJ 0.93) ran perfectly.  It took 3:39 hours (4 mins faster)
MAKE-ALL (Poly/ML) ran perfectly.  It took 3:23 hours (5 mins faster)

ZF/simpdata/ZF_ss: deleted anti_refl_rew; non-linear patterns slow down
discrimination nets (and this rewrite used only ONCE)

ZF/mem_not_refl: new; replaces obsolete anti_refl_rew

**Timing experiments**

fun HYP_SIMP_TAC ss = METAHYPS (fn hyps => HOL_SIMP_TAC (ss addrews hyps) 1);

On large examples such as ...
HOL/arith/mod_quo_equality 
HOL/llist/LListD_implies_ntrunc_equality
ZF/ex/bin/integ_of_bin_succ
... it is 1.5 to 3 times faster than ASM_SIMP_TAC.  But cannot replace
ASM_SIMP_TAC since the auto_tac sometimes fails due to lack of assumptions.
If there are few assumptions then HYP_SIMP_TAC is no better.

Pure/Makefile: now copies $(ML_DBASE) to $(BIN)/Pure instead of calling
make_database, so that users can call make_database for their object-logics.

Pure/tctical/SELECT_GOAL: now does nothing if i=1 and there is
only one subgoal.

19 April

MAKE-ALL (NJ 0.93) failed in HOL due to lack of disc space.
MAKE-ALL (Poly/ML) ran perfectly.  It took 3:23 hours 

**** Installation of new simplifier ****

Provers/simp/EXEC: now calls METAHYPS and passes the hyps as an extra arg
to the auto_tac.

FOL,HOL/simpdata: auto_tac now handles the hyps argument

ZF/simpdata/standard_auto_tac: deleted
ZF/simpdata/auto_tac: added hyps argument
ZF/epsilon/eclose_least_lemma: no special auto_tac 

*/ex/ROOT: no longer use 'cd' commands; instead pathnames contain "ex/..."

20 April

MAKE-ALL failed in HOL/Subst

HOL/Subst/setplus/cla_case: renamed imp_excluded_middle and simplified.
Old version caused ambiguity in rewriting:
     "[| P ==> P-->Q;  ~P ==> ~P-->Q |] ==> Q";

**** New tar file placed on /homes/lcp (????) **** 

Pure/Syntax: improvements to the printing of syntaxes
Pure/Syntax/lexicon.ML: added name_of_token
Pure/Syntax/earley0A.ML: updated print_gram

21 April

MAKE-ALL (NJ 0.93) ran perfectly.  It took 3:44 hours
MAKE-ALL (Poly/ML) failed in HOL due to lack of disc space

HOL/list,llist: now share NIL, CONS, List_Fun and List_case

make-all: now compresses the log files, which were taking up 4M; this
reduces their space by more than 1/3

rm-logfiles: now deletes compressed log files.

** Patrick Meche has noted that if the goal is stated with a leading !!
quantifier, then the list of premises is always empty -- this gives the
effect of an initial (cut_facts_tac prems 1).  The final theorem is the
same as it would be without the quantifier.

ZF: used the point above to simplify many proofs
ZF/domrange/cfast_tac: deleted, it simply called cut_facts_tac

22 April

MAKE-ALL (NJ 0.93) ran perfectly.  It took 3:52 hours??
MAKE-ALL (Poly/ML) ran perfectly.  It took 3:16 hours

30 April

HOL: installation of finite set notation: {x1,...,xn} (by Tobias Nipkow)

HOL/set.thy,set.ML,fun.ML,equalities.ML: addition of rules for "insert",
new derivations for "singleton"

HOL/llist.thy,llist.ML: changed {x.False} to {}

**** New tar file placed on /homes/lcp (584K) **** 

4 May

MAKE-ALL (NJ 0.93) ran out of space in LK.
MAKE-ALL (Poly/ML) ran perfectly.  It took 3:14 hours

Pure/Makefile: inserted "chmod u+w $(BIN)/Pure;" in case $(ML_DBASE) is
write-protected

5 May

HOL/list/not_Cons_self: renamed from l_not_Cons_l
HOL/list/not_CONS_self: new

HOL/llist.thy/Lconst: changed type and def to remove Leaf
HOL/llist.ML: changed Lconst theorems

6 May

MAKE-ALL (Poly/ML) ran perfectly.  It took 3:18 hours

** Installation of new HOL from Tobias **

HOL/ex/{finite,prop-log} made like the ZF versions
HOL/hol.thy: type classes plus, minus, times; overloaded operators + - *
HOL/set: set enumeration via "insert"
         additions to set_cs and set_ss
HOL/set,subset,equalities: various lemmas to do with {}, insert and -
HOL/llist: One of the proofs needs one fewer commands
HOL/arith: many proofs require type constraints due to overloading

** end Installation **

ZF/ex/misc: added new lemmas from Abrial's paper

7 May 

HOL/llist.ML/LList_corec_subset1: deleted a fast_tac call; the previous
simplification now proves the subgoal.

**** New tar file placed on /homes/lcp (584K) **** 

** Installation of new simplifier from Tobias **

The "case_splits" parameter of SimpFun is moved from the signature to the
simpset.  SIMP_CASE_TAC and ASM_SIMP_CASE_TAC are removed.  The ordinary
simplification tactics perform case splits if present in the simpset.

The simplifier finds out for itself what constant is affected.  Instead of
supplying the pair (expand_if,"if"), supply just the rule expand_if.

This change affects all calls to SIMP_CASE_TAC and all applications of SimpFun.

MAKE-ALL (Poly/ML) ran perfectly.  It took 3:18 hours

Cube/ex: UNTIL1, UNTIL_THM: replaced by standard tactics DEPTH_SOLVE_1 and
DEPTH_SOLVE

HOL: installation of NORM tag for simplication.  How was it forgotten??

HOL/hol.thy: declaration of NORM
HOL/simpdata: NORM_def supplied to SimpFun

10 May

MAKE-ALL (Poly/ML) ran perfectly.  It took 3:33 hours??

11 May

HOL/prod/Prod_eq: renamed Pair_eq
HOL/ex/lex-prod: wf_lex_prod: simplified proof

HOL/fun/inj_eq: new

HOL/llist/sumPairE: deleted, thanks to new simplifier's case splits!

12 May

MAKE-ALL (NJ 0.93) ran out of space in HOL.
MAKE-ALL (Poly/ML) failed in HOL.
HOL/Subst/utermlemmas/utlemmas_ss: deleted Prod_eq from the congruence rules

13 May

Pure/logic/flexpair: moved to term, with "equals" etc.  Now pervasive
Pure/logic/mk_flexpair: now exported
Pure/logic/dest_flexpair: new
Pure/goals/print_exn: now prints the error message for TERM and TYPE

Pure/Syntax/sextension: now =?= has type ['a::{}, 'a] => prop because
flexflex pairs can have any type at all.  Thus == must have the same type.

Pure/thm/flexpair_def: now =?= and == are equated for all 'a::{}.

Pure/tctical/equal_abs_elim,equal_abs_elim_list: new (for METAHYPS fix)
Pure/tctical/METAHYPS: now works if new proof state has flexflex pairs

Pure/Syntax/earley0A,syntax,lexicon: Tokens are represented by strings now,
not by integers.  (Changed by Tobias)

*** Installation of more printing functions ***

Pure/sign/sg: changed from a type abbrev to a datatype
Pure/type/type_sig: changed from a type abbrev to a datatype
These changes needed for abstract type printing in NJ

Pure/tctical/print_sg,print_theory: new

Pure/drule: new file containing derived rules and printing functions.
Mostly from tctical.ML, but includes rewriting rules from tactic.ML.

Pure/ROOT: loads drule before tctical; TacticalFun,TacticFun,GoalsFun now
depend on Drule and have sharing constraints.

14 May

Installing new print functions for New Jersey: incompatible with Poly/ML!

Pure/NJ/install_pp_nj: new (requires datatypes as above)
Pure/POLY/install_pp_nj: a dummy version

Pure/ROOT: calls install_pp_nj to install printing for NJ

*/ROOT: added extra install_pp calls (sg, theory, cterm, typ, ctyp) for
Poly/ML [ZF,LCF,Modal do not need them since they inherit them from another
logic -- make_database is not used]

17 May

MAKE-ALL (NJ 0.93) ran perfectly.  It took 3:57 hours??

Pure/Syntax/lexicon: Yet another leaner and faster version ... (from Tobias)

18 May

MAKE-ALL (Poly/ML) ran perfectly.  It took 3:36 hours

19 May

ZF/equalities/Union_singleton,Inter_singleton: now refer to {b} instead of
complex assumptions

20 May

HOL/list: Tobias added the [x1,...,xn] notation and the functions hd, tl,
null and list_case.

1 June

MAKE-ALL (Poly/ML) ran perfectly.  It took 3:39 hours

**** New tar file 92.tar.z placed on /homes/lcp (376K) **** 

MAKE-ALL (NJ 0.93) ran perfectly.  It took 1:49 hours on albatross.

Pure/tactic/dres_inst_tac,forw_inst_tac: now call the new
make_elim_preserve to preserve Var indexes when creating the elimination
rule.

ZF/ex/ramsey: modified calls to dres_inst_tac

2 June

Pure/Thy/read/read_thy,use_thy: the .thy.ML file is now written to the
current directory, since the pathname may lead to a non-writeable area.

HOL/arith: renamed / and // to div and mod
ZF/arith: renamed #/ and #// to div and mod

MAKE-ALL (Poly/ML) ran perfectly.  It took 1:48 hours on albatross.

**** New tar file 92.tar.z placed on /homes/lcp (376K) **** 

Pure/NJ/commit: new dummy function
FOLP/ex/ROOT: inserted commit call to avoid Poly/ML problems

make-all: now builds FOLP also!

3 June

ZF/zf.thy,HOL/list.thy,HOL/set.thy: now constructions involving {_}, [_],
<_,_> are formatted as {(_)}, [(_)], 

MAKE-ALL (Poly/ML) ran perfectly.  It took 4:37 hours on muscovy (with FOLP).

ZF/Makefile: removed obsolete target for .rules.ML

All object-logic Makefiles: EXAMPLES ARE NO LONGER SAVED.  This saves disc
and avoids problems (in New Jersey ML) of writing to the currently
executing image.

4 June

Pure/logic/rewritec: now uses nets for greater speed.  Functor LogicFun now
takes Net as argument.

Pure/ROOT: now loads net before logic.

MAKE-ALL (Poly/ML) failed in ZF and HOL.

LK/lk.thy: changed constant "not" to "Not" (for consistency with FOL)

7 June

Pure/tactic/is_letdig: moved to library
Pure/Syntax/lexicon/is_qld: deleted, was same as is_letdig

MAKE-ALL (Poly/ML) ran perfectly.  It took 2:07 hours on albatross.
MAKE-ALL (NJ 0.93) ran perfectly.  It took 4:41 hours on dunlin.

HOL/set/UN1,INT1: new union/intersection operators.  Binders UN x.B(x),
INT x.B(x).

HOL/univ,llist: now use UN x.B(x) instead of Union(range(B))

HOL/subset: added lattice properties for INT, UN (both forms)

8 June

MAKE-ALL (NJ 0.93) ran perfectly.  It took 4:45 hours on dunlin.

**** New tar file 92.tar.z placed on /homes/lcp (384K) **** 

14 June

HOL/list.thy/List_rec_def: changed pred_sexp (a variable!) to pred_Sexp.
Using def_wfrec hides such errors!!

**** New tar file 92.tar.gz placed on /homes/lcp (384K) **** 

** NEW VERSION FROM MUNICH WITH ==-REWRITING **

** The following changes are Toby's **

type.ML:

Renamed mark_free to freeze_vars and thaw_tvars to thaw_vars.
Added both functions to the signature.

sign.ML:

Added val subsig: sg * sg -> bool to signature.
Added trueprop :: prop and mark_prop : prop => prop to pure_sg.

Added

val freeze_vars: term -> term
val thaw_vars: term -> term
val strip_all_imp: term * int -> term list * term * int

Moved rewritec_bottom and rewritec_top to thm.ML.
Only bottom-up rewriting supported any longer.

thm.ML:

Added

(* internal form of conditional ==-rewrite rules *)
type meta_simpset
val add_mss: meta_simpset * thm list -> meta_simpset
val empty_mss: meta_simpset
val mk_mss: thm list -> meta_simpset

val mark_prop_def: thm
val truepropI: thm
val trueprop_def: thm

(* bottom-up conditional ==-rewriting with local ==>-assumptions *)
val rewrite_cterm: meta_simpset -> (thm -> thm list)
                   -> (meta_simpset -> thm list -> Sign.cterm -> thm)
                   -> Sign.cterm -> thm
val trace_simp: bool ref

Simplified concl_of: call to Logic.skip_flexpairs redundant.

drule.ML:

Added

(* rewriting *)
val asm_rewrite_rule: (thm -> thm list) -> thm list -> thm -> thm
val rewrite_goal_rule: (thm -> thm list) -> thm list -> int -> thm -> thm
val rewrite_goals_rule: (thm -> thm list) -> thm list -> thm -> thm

(* derived concepts *)
val forall_trueprop_eq: thm
val implies_trueprop_eq: thm
val mk_trueprop_eq: thm -> thm
val reflexive_eq: thm
val reflexive_thm: thm
val trueprop_implies_eq: thm
val thm_implies: thm -> thm -> thm
val thm_equals: thm -> thm -> thm

(*Moved here from tactic.ML:*)
val asm_rl: thm
val cut_rl: thm
val revcut_rl: thm

tactic.ML:

Added

val asm_rewrite_goal_tac: (thm -> thm list) -> thm list -> int -> tactic
val asm_rewrite_goals_tac: (thm -> thm list) -> thm list -> tactic
val asm_rewrite_tac: (thm -> thm list) -> thm list -> tactic
val fold_goal_tac: thm list -> int -> tactic
val rewrite_goal_tac: thm list -> int -> tactic

Moved to drule.ML:
val asm_rl: thm
val cut_rl: thm
val revcut_rl: thm

goals.ML:

Changed prepare_proof to make sure that rewriting with empty list of
meta-thms is identity.

** End of Toby's changes **

16 June

Pure/sign/typ_of,read_ctyp: new
Pure/logic/dest_flexpair: now exported

Pure/drule/flexpair_intr,flexpair_elim: new; fixes a bug in
flexpair_abs_elim_list

HOL/equalities/image_empty,image_insert: new
HOL/ex/finite/Fin_imageI: new

Installed Martin Coen's CCL as new object-logic

17 June

** More changes from Munich (Markus Wenzel) **

Pure/library: added the, is_some, is_none, separate and improved space_implode
Pure/sign: Sign.extend now calls Syntax.extend with list of constants
Pure/symtab: added is_null
Pure/Syntax/sextension: added empty_sext
Pure/Syntax/syntax: changed Syntax.extend for compatibility with future version

HOL now exceeds poly's default heap size. Hence HOL/Makefile needs to
specify -h 8000.

HOL/univ/ntrunc_subsetD, etc: deleted the useless j<k assumption

18 June

MAKE-ALL (Poly/ML) ran perfectly.  It took 4:59 hours on dunlin (with CCL).

Pure/sign/read_def_cterm: now prints the offending terms, as well as the
types, when exception TYPE is raised.

HOL/llist: some tidying

23 June

HOL/llist/Lconst_type: generalized from Lconst(M): LList({M})

24 June

MAKE-ALL (Poly/ML) ran perfectly.  It took 2:23 hours on albatross (with CCL)

MAKE-ALL (NJ 0.93) failed in CCL due to use of "abstraction" as an
identifier in CCL.ML

**** New tar file 92.tar.gz placed on /homes/lcp (384K) **** (with CCL)

CCL/ROOT: added ".ML" extension to use commands for NJ compatibility

25 June

MAKE-ALL (Poly/ML) ran perfectly.  It took 2:23 hours on albatross.
MAKE-ALL (NJ 0.93) failed in HOL due to lack of ".ML" extension

HOL/fun/rangeE,imageE: eta-expanded f to get variable name preservation

HOL/llist/iterates_equality,lmap_lappend_distrib: tidied

28 June

HOL/set/UN1_I: made the Var and Bound variables agree ("x") to get variable
name preservation 

HOL/llist: co-induction rules applied with res_inst_tac to state the
bisimulation directly

2 July

MAKE-ALL (NJ 0.93) ran perfectly.  It took 2:10 hours on albatross.
MAKE-ALL (Poly/ML) ran perfectly.  It took 2:23 hours on albatross.

92/Makefile/$(BIN)/Pure: changed echo makefile= to echo database=

**** New tar file 92.tar.gz placed on /homes/lcp (424K) **** (with CCL)


** NEW VERSION FROM MUNICH WITH ABSTRACT SYNTAX TREES & NEW PARSER **

I have merged in the changes shown above since 24 June

CHANGES LOG OF Markus Wenzel (MMW)
=======

29-Jun-1993 MMW
  *** Beta release of new syntax module ***
  (should be 99% backwards compatible)

  Pure/Thy/ROOT.ML
    added keywords for "translations" section

  Pure/Thy/syntax.ML
    minor cleanup
    added syntax for "translations" section
    .*.thy.ML files now human readable
    .*.thy.ML used to be generated incorrectly if no mixfix but "ML" section
    "ML" section no longer demands any definitions (parse_translation, ...)

  Pure/Thy/read.ML
    read_thy: added close_in
    added file_exists (not perfect)
    use_thy: now uses file_exists

  Pure/thm.ML
    added syn_of: theory -> syntax

  Pure/Makefile
    SYNTAX_FILES: added Syntax/ast.ML

  Pure/Syntax/pretty.ML
    added str_of: T -> string

  Pure/Syntax/ast.ML
    added this file

  Pure/Syntax/extension.ML
  Pure/Syntax/parse_tree.ML
  Pure/Syntax/printer.ML
  Pure/Syntax/ROOT.ML
  Pure/Syntax/sextension.ML
  Pure/Syntax/syntax.ML
  Pure/Syntax/type_ext.ML
  Pure/Syntax/xgram.ML
    These files have been completely rewritten, though the global structure
    is similar to the old one.


30-Jun-1993 MMW
  New versions of HOL and Cube: use translation rules wherever possible;

  HOL/hol.thy
    cleaned up
    removed alt_tr', mk_bindopt_tr'
    alternative binders now implemented via translation rules and mk_alt_ast_tr'

  HOL/set.thy
    cleaned up
    removed type "finset"
    now uses category "args" for finite sets
    junked "ML" section
    added "translations" section

  HOL/list.thy
    cleaned up
    removed type "listenum"
    now uses category "args" for lists
    junked "ML" section
    added "translations" section

  Cube/cube.thy
    cleaned up
    changed indentation of Lam and Pi from 2 to 3
    removed qnt_tr, qnt_tr', no_asms_tr, no_asms_tr'
    fixed fun_tr': all but one newly introduced frees will have type dummyT
    added "translations" section


30-Jun-1993, 05-Jul-1993 MMW
  Improved toplevel pretty printers:
    - unified interface for POLY and NJ;
    - print functions now insert atomic string into the toplevel's pp stream,
      rather than writing it to std_out (advantage: output appears at the
      correct position, disadvantage: output cannot be broken);
  (Is there anybody in this universe who exactly knows how Poly's install_pp
  is supposed to work?);

  Pure/NJ.ML
    removed dummy install_pp
    added make_pp, install_pp

  Pure/POLY.ML
    removed dummy install_pp_nj
    added make_pp

  Pure/ROOT.ML
    removed install_pp_nj stuff

  Pure/drule.ML
    added str_of_sg, str_of_theory, str_of_thm

  Pure/install_pp.ML
    added this file

  Pure/sign.ML
    added str_of_term, str_of_typ, str_of_cterm, str_of_ctyp

  Pure/goals.ML
    added str_of_term, str_of_typ

  CTT/ROOT.ML
  Cube/ROOT.ML
  FOL/ROOT.ML
  FOLP/ROOT.ML
  HOL/ROOT.ML
  LK/ROOT.ML
    replaced install_pp stuff by 'use "../Pure/install_pp.ML"'


01-Jul-1993 MMW
  Misc small fixes

  CCL/ROOT.ML
  HOL/ROOT.ML
    added ".ML" suffix to some filenames

  HOL/ex/unsolved.ML
    replaced HOL_Rule.thy by HOL.thy

  Pure/NJ.ML
    quit was incorrectly int -> unit

END MMW CHANGES

Pure/Syntax/sextension/eta_contract: now initially false 

Pure/library/cat_lines: no longer calls "distinct"
Pure/sign: replaced to calls of implode (map (apr(op^,"\n") o ... by cat_lines
NB This could cause duplicate error messages from Pure/sign and Pure/type

Pure/goals/prove_goalw: now prints some of the information from print_exn

9 July

MAKE-ALL (Poly/ML) ran perfectly.  It took 2:26 hours on albatross.

**** New tar file 93.tar.gz placed on /homes/lcp (480K) **** 

12 July

MAKE-ALL (NJ 0.93) ran perfectly.  It took 2:13 hours on albatross.
MAKE-ALL (Poly/ML) ran perfectly.  It took 2:25 hours on albatross.

22 July

ZF/zf.thy: new version from Marcus Wenzel

ZF: ** installation of inductive definitions **

changing the argument order of "split"; affects fst/snd too
sum.thy zf.thy ex/bin.thy ex/integ.thy ex/simult.thy ex/term.thy
pair.ML  ex/integ.ML

changing the argument order of "case" and adding "Part": sum.thy sum.ML

ZF/zf.ML/rev_subsetD,rev_bspec: new

ZF/mono: new rules for implication
ZF/mono/Collect_mono: now for use with implication rules

ZF/zf.ML/ballE': renamed rev_ballE

ZF/list.thy,list.ML: files renamed list-fn.thy, list-fn.ML
ZF/list.ML: new version simply holds the datatype definition
NB THE LIST CONSTRUCTORS ARE NOW Nil/Cons, not 0/Pair.

ZF/extend_ind.ML, datatype.ML: new files
ZF/fin.ML: moved from ex/finite.ML

23 July

ZF/ex/sexp: deleted this example -- it seems hardly worth the trouble of
porting.

ZF/ex/bt.thy,bt.ML: files renamed bt-fn.thy, bt-fn.ML
ZF/ex/bt.ML: new version simply holds the datatype definition

ZF/ex/term.thy,term.ML: files renamed term-fn.thy, term-fn.ML
ZF/ex/term.ML: new version simply holds the datatype definition

ZF/sum/InlI,InrI: renamed from sum_InlI, sum_InlI

26 July

ZF/univ/rank_ss: new, for proving recursion equations

ZF/domrange/image_iff,image_singleton_iff,vimage_iff,vimage_singleton_iff,
field_of_prod:new

ZF/domrange/field_subset: modified

ZF/list/list_cases: no longer proved by induction!
ZF/wf/wf_trancl: simplified proof

ZF/equalities: new laws for field

29 July

ZF/trancl/trancl_induct: new
ZF/trancl/rtrancl_induct,trancl_induct: now with more type information

** More changes from Munich (Markus Wenzel) **

Update of new syntax module (aka macro system): mostly internal cleanup and
polishing;

  Pure/Syntax/*
    added Ast.stat_norm
    added Syntax.print_gram, Syntax.print_trans, Syntax.print_syntax
    cleaned type and Pure syntax: "_CLASSES" -> "classes", "_SORTS" -> "sorts",
     "_==>" -> "==>", "_fun" -> "fun", added some space for printing
    Printer: partial fix of the "PROP <aprop>" problem: print "PROP " before
      any Var or Free of type propT
    Syntax: added ndependent_tr, dependent_tr'

  Pure/sign.ML: removed declaration of "==>" (now in Syntax.pure_sext)

Changes to object logics: minor cleanups and replacement of most remaining ML
translations by rewrite rules (see also file "Translations");

  ZF/zf.thy
    added "translations" section
    removed all parse/print translations except ndependent_tr, dependent_tr'
    fixed dependent_tr': all but one newly introduced frees have type dummyT
    replaced id by idt in order to make terms rereadable if !show_types

  Cube/cube.thy
    removed necontext
    replaced fun_tr/tr' by ndependent_tr/dependent_tr'

  CTT/ctt.thy
    added translations rules for PROD and SUM
    removed dependent_tr
    removed definitions of ndependent_tr, dependent_tr'

  HOL/set.thy: replaced id by idt

  CCL/ROOT.ML: Logtic -> Logic

  CCL/set.thy
    added "translations" section
    removed "ML" section
    replaced id by idt

  CCL/types.thy
    added "translations" section
    removed definitions of ndependent_tr, dependent_tr'
    replaced id by idt

Yet another improvement of toplevel pretty printers: output now breakable;

  Pure/NJ.ML Pure/POLY.ML improved make_pp

  Pure/install_pp.ML: replaced str_of_* by pprint_*

  Pure/drule.ML: replaced str_of_{sg,theory,thm} by pprint_*

  Pure/sign.ML: replaced str_of_{term,typ,cterm,ctyp} by pprint_*

  Pure/goals.ML: fixed and replaced str_of_{term,typ} by pprint_*

  Pure/Syntax/pretty.ML: added pprint, quote

Minor changes and additions;

  Pure/sign.ML: renamed stamp "PURE" to "Pure"

  Pure/library.ML
    added quote: string -> string
    added to_lower: string -> bool

  Pure/NJ.ML,POLY.ML: added file_info of Carsten Clasohm

30 July

MAKE-ALL (Poly/ML) ran perfectly.

Pure/goals/print_sign_exn: new, takes most code from print_exn
Pure/goals/prove_goalw: displays exceptions using print_sign_exn

Pure/drule/print_sg: now calls pretty_sg to agree with pprint_sg

Pure/library,...: replaced front/nth_tail by take/drop.

Pure/term/typ_tfrees,typ_tvars,term_tfrees,term_tvars: new
thm/mk_rew_triple, drule/types_sorts, sign/zero_tvar_indices: now use the above

Pure/logic/add_term_vars,add_term_frees,insert_aterm,atless:
moved to term, joining similar functions for type variables;
Logic.vars and Logic.frees are now term_vars and term_frees

Pure/term/subst_free: new

Pure/tactic/is_fact: newly exported

Provers/simp/mk_congs: uses filter_out is_fact to delete trivial cong rules

Pure/tactic/rename_last_tac: now uses Syntax.is_identifier instead of
forall is_letdig

**** New tar file 93.tar.gz placed on /homes/lcp (448K) **** 

2 August

MAKE-ALL (NJ 0.93) failed in ZF due to Compiler bug: elabDecl:open:FctBodyStr
MAKE-ALL (Poly/ML) failed in ZF/enum.  It took 2:33 hours on albatross.

Pure/drule/triv_forall_equality: new
Pure/tactic/prune_params_tac: new

Provers/hypsubst/bound_hyp_subst_tac: new, safer than hyp_subst_tac

3 August

Pure/tactic/rule_by_tactic: new

ZF/perm/compEpair: now proved via rule_by_tactic

ZF/extend_ind/cases,mk_cases: new
ZF/datatype/mk_free: new
ZF/list: now calls List.mk_cases

4 August

Provers/slow_tac,slow_best_tac: new

5 August

MAKE-ALL (Poly/ML) failed in ZF

ZF/sum/sumE2: deleted since unused
ZF/sum/sum_iff,sum_subset_iff,sum_equal_iff: new
ZF/univ/Transset_Vfrom: new; used in proof of Transset_Vset

6 August

Pure/goals/prepare_proof: after "Additional hypotheses", now actually
prints them!

ZF/ordinal/Transset_Union_family, Transset_Inter_family: renamed from
Transset_Union, Transset_Inter

ZF/ordinal/Transset_Union: new 
ZF/univ/pair_in_univ: renamed Pair_in_univ

ZF/mono/product_mono: generalized to Sigma_mono; changed uses in trancl, univ

ZF/lfp/lfp_Tarski,def_lfp_Tarski: renamed from Tarski,def_Tarski; changed
uses in extend_ind.ML, nat.ML, trancl.ML.

ZF/ex/misc: Schroeder-Bernstein Theorem moved here from lfp.ML

ZF/fixedpt.thy,.ML: renamed from lfp.thy,.ML, and gfp added

9 August

ZF/zf.thy/ndependent_tr,dependent_tr': deleted, since they are now on
Syntax/sextension. 

11 August

Pure/library.ML: added functions
assocs: (''a * 'b list) list -> ''a -> 'b list
transitive_closure: (''a * ''a list) list -> (''a * ''a list) list

Pure/type.ML: deleted (inefficient) transitive_closure