clasohm@0: EDITS TO THE ISABELLE SYSTEM FOR 1993
clasohm@0: 
clasohm@0: 11 January 
clasohm@0: 
clasohm@0: */README: Eliminated references to Makefile.NJ, which no longer exists.
clasohm@0: 
clasohm@0: **** New tar file placed on /homes/lcp (464K) **** 
clasohm@0: 
clasohm@0: 14 January
clasohm@0: 
clasohm@0: Provers/simp/pr_goal_lhs: now distinct from pr_goal_concl so that tracing
clasohm@0: prints conditions correctly.
clasohm@0: 
clasohm@0: {CTT/arith,HOL/ex/arith/ZF/arith}/add_mult_distrib: renamed from
clasohm@0: add_mult_dist, to agree with the other _distrib rules
clasohm@0: 
clasohm@0: 20 January
clasohm@0: 
clasohm@0: Pure/Syntax/type_ext.ML: "I have fixed a few anomalies in the pretty
clasohm@0: printing annotations for types.  Only the layout has changed." -- Toby
clasohm@0: 
clasohm@0: 21 January
clasohm@0: 
clasohm@0: {CTT/arith,HOL/ex/arith/ZF/arith}/add_inverse_diff: renamed to add_diff_inverse
clasohm@0: 
clasohm@0: 22 January
clasohm@0: 
clasohm@0: ZF/ex/equiv: new theory of equivalence classes
clasohm@0: ZF/ex/integ: new theory of integers
clasohm@0: HOL/set.thy: added indentation of 3 to all binding operators
clasohm@0: 
clasohm@0: ZF/bool/boolI0,boolI1: renamed as bool_0I, bool_1I
clasohm@0: 
clasohm@0: 25 January
clasohm@0: 
clasohm@0: MAKE-ALL (NJ 0.75) ran perfectly.  It took 3:19 hours!?
clasohm@0: 
clasohm@0: ZF/bool/not,and,or,xor: new
clasohm@0: 
clasohm@0: 27 January
clasohm@0: 
clasohm@0: ZF/ex/bin: new theory of binary integer arithmetic
clasohm@0: 
clasohm@0: 27 January
clasohm@0: 
clasohm@0: MAKE-ALL (Poly/ML) ran perfectly.  It took 6:33 hours???
clasohm@0: (ZF took almost 5 hours!)
clasohm@0: 
clasohm@0: **** New tar file placed on /homes/lcp (472K) **** 
clasohm@0: 
clasohm@0: HOL/set/UN_cong,INT_cong: new
clasohm@0: HOL/subset/mem_rews,set_congs,set_ss: new
clasohm@0: HOL/simpdata/o_apply: new; added to HOL_ss
clasohm@0: 
clasohm@0: 29 January
clasohm@0: 
clasohm@0: Pure/Thy/syntax/mk_structure: the dummy theory created by type infixes is
clasohm@0: now called name^"(type infix)" instead of "", avoid triggering a spurious
clasohm@0: error "Attempt to merge different versions of theory: " in
clasohm@0: Pure/sign/merge_stamps
clasohm@0: 
clasohm@0: 2 February
clasohm@0: 
clasohm@0: MAKE-ALL (Poly/ML) ran perfectly.  It took 2:48 hours.  Runs in 1992 took
clasohm@0: under 2:20 hours, but the new files in ZF/ex take time: nearly 23 minutes
clasohm@0: according to make10836.log.
clasohm@0: 
clasohm@0: Pure/Thy/scan/comment: renamed from komt
clasohm@0: Pure/Thy/scan/numeric: renamed from zahl
clasohm@0: 
clasohm@0: Pure/Syntax/syntax,lexicon,type_ext,extension,sextension: modified by
clasohm@0: Tobias to change ID, TVAR, ... to lower case.
clasohm@0: 
clasohm@0: Cube/cube.thy,HOL/hol.thy,HOL/set.thy,CTT/ctt.thy,LK/lk.thy,ZF/zf.thy: now
clasohm@0: with ID, ... in lower case and other tidying
clasohm@0: 
clasohm@0: 3 February
clasohm@0: 
clasohm@0: MAKE-ALL (Poly/ML) ran perfectly.  It took 2:50 hours.
clasohm@0: 
clasohm@0: 4 February
clasohm@0: 
clasohm@0: HOL/nat/nat_ss: now includes the rule Suc_less_eq: (Suc(m) < Suc(n)) = (m<n)
clasohm@0: and the nat_case rules and congruence rules
clasohm@0: 
clasohm@0: HOL/sum/sumE: now has the "strong" form with equality assumptions.  WAS
clasohm@0:     val prems = goalw Sum.thy [Inl_def,Inr_def]
clasohm@0: 	"[| !!x::'a. P(Inl(x));  !!y::'b. P(Inr(y)) \
clasohm@0:     \    |] ==> P(s)";
clasohm@0:     by (res_inst_tac [("t","s")] (Rep_Sum_inverse RS subst) 1);
clasohm@0:     by (rtac (rewrite_rule [Sum_def] Rep_Sum RS CollectE) 1);
clasohm@0:     by (REPEAT (eresolve_tac [disjE,exE,ssubst] 1 ORELSE resolve_tac prems 1));
clasohm@0:     val sumE = result();
clasohm@0: 
clasohm@0: 8 February
clasohm@0: 
clasohm@0: Changes from Tobias:
clasohm@0: Pure/Thy/parse: now list_of admits the empty phrase, while listof_1 does not
clasohm@0: Pure/Thy/syntax: uses new list_of, list_of1
clasohm@0: 
clasohm@0: 9 February
clasohm@0: 
clasohm@0: HOL/ex/arith: moved to main HOL directory
clasohm@0: HOL/prod: now define the type "unit" and constant "(): unit"
clasohm@0: 
clasohm@0: 11 February
clasohm@0: 
clasohm@0: HOL/arith: eliminated redefinitions of nat_ss and arith_ss
clasohm@0: 
clasohm@0: 12 February
clasohm@0: 
clasohm@0: MAKE-ALL (Poly/ML) ran perfectly.  It took 2:50 hours.
clasohm@0: 
clasohm@0: Pure/Thy/scan/string: now correctly recognizes ML-style strings.
clasohm@0: 
clasohm@0: 15 February
clasohm@0: 
clasohm@0: MAKE-ALL (NJ 0.75) ran perfectly.  It took 1:37 hours (on albatross)
clasohm@0: MAKE-ALL (NJ 0.75) ran perfectly.  It took 2:42 hours (on dunlin)
clasohm@0: MAKE-ALL (Poly/ML) ran perfectly.  It took 2:53 hours (on dunlin)
clasohm@0: 
clasohm@0: **** New tar file placed on /homes/lcp (480K) **** 
clasohm@0: 
clasohm@0: 18 February
clasohm@0: 
clasohm@0: Pure/Syntax/earley0A/compile_xgram: Tobias deleted the third argument, as
clasohm@0: it was unused.
clasohm@0: 
clasohm@0: Pure/Syntax/earley0A: modified accordingly.
clasohm@0: 
clasohm@0: 19 February
clasohm@0: 
clasohm@0: MAKE-ALL (NJ 0.75) ran perfectly.  It took 3:37 hours 
clasohm@0: MAKE-ALL (Poly/ML) ran perfectly.  It took 2:52 hours
clasohm@0: 
clasohm@0: **** New tar file placed on /homes/lcp (480K) **** 
clasohm@0: 
clasohm@0: 20 February
clasohm@0: 
clasohm@0: MAKE-ALL (NJ 0.93) ran perfectly.  It took 3:30 hours 
clasohm@0: 
clasohm@0: 10 March
clasohm@0: 
clasohm@0: HOL/fun/image_eqI: fixed bad pattern
clasohm@0: 
clasohm@0: 11 March
clasohm@0: 
clasohm@0: MAKE-ALL (Poly/ML) failed in HOL!
clasohm@0: 
clasohm@0: HOL/fun: moved "mono" proofs to HOL/subset, since they rely on subset laws
clasohm@0: of Int and Un.
clasohm@0: 
clasohm@0: 12 March
clasohm@0: 
clasohm@0: ZF/ex/misc: new example from Bledsoe
clasohm@0: 
clasohm@0: 15 March
clasohm@0: 
clasohm@0: ZF/perm: two new theorems inspired by Pastre
clasohm@0: 
clasohm@0: 16 March
clasohm@0: 
clasohm@0: Weakened congruence rules for HOL: speeds simplification considerably by
clasohm@0: NOT simplifying the body of a conditional or eliminator.
clasohm@0: 
clasohm@0: HOL/simpdata/mk_weak_congs: new, to make weakened congruence rules
clasohm@0: 
clasohm@0: HOL/simpdata/congs: renamed HOL_congs and weakened the "if" rule
clasohm@0: 
clasohm@0: HOL/simpdata/HOL_congs: now contains polymorphic rules for the overloaded
clasohm@0: operators < and <=
clasohm@0: 
clasohm@0: HOL/prod: weakened the congruence rule for split
clasohm@0: HOL/sum: weakened the congruence rule for case
clasohm@0: HOL/nat: weakened the congruence rule for nat_case and nat_rec
clasohm@0: HOL/list: weakened the congruence rule for List_rec and list_rec
clasohm@0: 
clasohm@0: HOL & test rebuilt perfectly
clasohm@0: 
clasohm@0: Pure/goals/prepare_proof/mkresult: fixed bug in signature check.  Now
clasohm@0: compares the FINAL signature with that from the original theory.
clasohm@0: 
clasohm@0: Pure/goals/prepare_proof: ensures that [prove_]goalw checks that the
clasohm@0: definitions do not update the proof state.
clasohm@0: 
clasohm@0: 17 March
clasohm@0: 
clasohm@0: MAKE-ALL (Poly/ML) ran perfectly.
clasohm@0: 
clasohm@0: 18 March
clasohm@0: 
clasohm@0: MAKE-ALL (Poly/ML) failed in HOL/ex/Substitutions
clasohm@0: 
clasohm@0: HOL/ex/Subst/setplus: changed Set.thy to Setplus.thy where
clasohm@0: necessary
clasohm@0: 
clasohm@0: ZF/perm: proved some rules about inj and surj
clasohm@0: 
clasohm@0: ZF/ex/misc: did some of Pastre's examples
clasohm@0: 
clasohm@0: Pure/library/gen_ins,gen_union: new
clasohm@0: 
clasohm@0: HOL/ex/Subst/subst: renamed rangeE to srangeE
clasohm@0: 
clasohm@0: 18 March
clasohm@0: 
clasohm@0: MAKE-ALL (Poly/ML) failed in HOL/ex/term due to renaming of list_ss in
clasohm@0: ex/Subst/alist
clasohm@0: 
clasohm@0: HOL/list/list_congs: new; re-organized simpsets a bit
clasohm@0: 
clasohm@0: Pure/goals/sign_error: new
clasohm@0: 
clasohm@0: Pure/goals/prepare_proof,by_com: now print the list of new theories when
clasohm@0: the signature of the proof state changes 
clasohm@0: 
clasohm@0: HOL/prod,sexp: renamed fst, snd to fst_conv, snd_conv to avoid over-writing
clasohm@0: the library functions fst, snd
clasohm@0: 
clasohm@0: HOL/fun/image_compose: new
clasohm@0: 
clasohm@0: 21 March
clasohm@0: 
clasohm@0: MAKE-ALL (NJ 0.93) ran perfectly.  It took 3:50 hours 
clasohm@0: MAKE-ALL (Poly/ML) ran perfectly.  It took 3:21 hours
clasohm@0: Much slower now (about 30 minutes!) because of HOL/ex/Subst
clasohm@0: 
clasohm@0: **** New tar file placed on /homes/lcp (504K) **** 
clasohm@0: 
clasohm@0: ZF/pair,simpdata: renamed fst, snd to fst_conv, snd_conv to avoid over-writing
clasohm@0: the library functions fst, snd
clasohm@0: 
clasohm@0: HOL/prod/prod_fun_imageI,E: new
clasohm@0: 
clasohm@0: HOL/ex/Subst/Unify: renamed to Unifier to avoid clobbering structure Unify
clasohm@0: of Pure
clasohm@0: 
clasohm@0: 24 March
clasohm@0: 
clasohm@0: HOL/trancl/comp_subset_Sigma: new
clasohm@0: HOL/wf/wfI: new
clasohm@0: 
clasohm@0: HOL/Subst: moved from HOL/ex/Subst to shorten pathnames
clasohm@0: HOL/Makefile: target 'test' now loads Subst/ROOT separately
clasohm@0: 
clasohm@0: *** Installation of gfp, coinduction, ... to HOL ***
clasohm@0: 
clasohm@0: HOL/gfp,llist: new
clasohm@0: HOL/univ,sexp,list: replaced with new version
clasohm@0: 
clasohm@0: Sexp is now the set of all well-founded trees, each of type 'a node set.
clasohm@0: There is no longer a type 'sexp'.  Initial algebras require more explicit
clasohm@0: type checking than before.  Defining a type 'sexp' would eliminate this,
clasohm@0: but would also require a whole new set of primitives, similar to those
clasohm@0: defined in univ.thy but restricted to well-founded trees.
clasohm@0: 
clasohm@0: 25 March
clasohm@0: 
clasohm@0: Pure/thm: renamed 'bires' to 'eres' in many places (not exported) --
clasohm@0: biresolution now refers to resolution with (flag,rule) pairs.
clasohm@0: 
clasohm@0: Pure/thm/bicompose_aux: SOUNDNESS BUG concerning variable renaming.  A Var in
clasohm@0: a premise was getting renamed when its occurrence in the flexflex pairs was
clasohm@0: not.  Martin Coen supplied the following proof of True=False in HOL:
clasohm@0: 
clasohm@0:     val [prem] = goal Set.thy "EX a:{c}.p=a ==> p=c";
clasohm@0:     br (prem RS bexE) 1; be ssubst 1; be singletonD 1;
clasohm@0:     val l1 = result();
clasohm@0: 
clasohm@0:     val rls = [refl] RL [bexI] RL [l1];
clasohm@0: 
clasohm@0:     goal Set.thy "True = False";
clasohm@0:     brs rls 1; br singletonI 1;
clasohm@0:     result();
clasohm@0: 
clasohm@0: Marcus Moore noted that the error only occurred with
clasohm@0: Logic.auto_rename:=false.  Elements of the fix:
clasohm@0: 
clasohm@0: 1.  rename_bvs, rename_bvars and bicompose_aux/newAs take tpairs (the
clasohm@0: existing flex-flex pairs) as an extra argument.  rename_bvs preserves all
clasohm@0: Vars in tpairs.
clasohm@0: 
clasohm@0: 2.  bicompose_aux/tryasms and res now unpack the "cell" and supply its tpairs
clasohm@0: to newAs.
clasohm@0: 
clasohm@0: HOL/lfp,gfp,ex/set: renamed Tarski to lfp_Tarski
clasohm@0: 
clasohm@0: HOL/lfp,list,llist,nat,sexp,trancl,Subst/uterm,ex/simult,ex/term: renamed
clasohm@0: def_Tarski to def_lfp_Tarski 
clasohm@0: 
clasohm@0: 26 March
clasohm@0: 
clasohm@0: MAKE-ALL (NJ 0.93) ran perfectly.  It took 4:25 hours!
clasohm@0: MAKE-ALL (Poly/ML) ran perfectly.  It took 3:54 hours! (jobs overlapped)
clasohm@0: 
clasohm@0: Pure/Thy/scan/is_digit,is_letter: deleted.  They are already in
clasohm@0: Pure/library, and these versions used non-Standard string comparisons!
clasohm@0: 
clasohm@0: Repairing a fault reported by David Aspinall:
clasohm@0:   show_types := true;  read "a";  (* followed by  'prin it' for NJ *)
clasohm@0: Raises exception  LIST "hd".   Also has the side effect of leaving
clasohm@0: show_types set at false. 
clasohm@0: 
clasohm@0: Pure/goals/read: no longer creates a null TVar
clasohm@0: Pure/Syntax/lexicon/string_of_vname: now handles null names
clasohm@0: Pure/Syntax/printer/string_of_typ: tidied
clasohm@0: 
clasohm@0: /usr/groups/theory/isabelle/92/Pure/thm: replaced by new version to fix bug
clasohm@0: MAKE-ALL on this directory ran perfectly
clasohm@0: /usr/groups/theory/ml-aftp/Isabelle92.tar.Z: replaced by new version
clasohm@0: 
clasohm@0: 29 March
clasohm@0: 
clasohm@0: MAKE-ALL (NJ 0.93) ran perfectly.  It took 4:14 hours!
clasohm@0: MAKE-ALL (Poly/ML) ran perfectly.  It took 3:43 hours!
clasohm@0: 
clasohm@0: **** New tar file placed on /homes/lcp (518K) **** 
clasohm@0: 
clasohm@0: 30 March
clasohm@0: 
clasohm@0: ZF/univ/cons_in_Vfrom: deleted "[| a: Vfrom(A,i);  b<=Vfrom(A,i) |] ==>
clasohm@0: cons(a,b) : Vfrom(A,succ(i))" since it was useless.
clasohm@0: 
clasohm@0: 8 April
clasohm@0: 
clasohm@0: MAKE-ALL (Poly/ML) ran perfectly.  It took 3:49 hours!
clasohm@0: 
clasohm@0: **** New tar file placed on /homes/lcp (520K) **** 
clasohm@0: 
clasohm@0: **** Updates for pattern unification (Tobias Nipkow) ****
clasohm@0: 
clasohm@0: Pure/pattern.ML: new, pattern unification
clasohm@0: 
clasohm@0: Pure/Makefile and ROOT.ML: included pattern.ML
clasohm@0: 
clasohm@0: Pure/library.ML: added predicate downto0
clasohm@0: 
clasohm@0: Pure/unify.ML: call pattern unification first. Removed call to could_unify.
clasohm@0: 
clasohm@0: FOL/Makefile/FILES: now mentions ifol.ML (previously repeated fol.ML instead)
clasohm@0: 
clasohm@0: **** Installation of Martin Coen's FOLP (FOL + proof objects) ****
clasohm@0: 
clasohm@0: renamed PFOL, PIFOL to FOLP, IFOLP, etc.
clasohm@0: 
clasohm@0: 9 April
clasohm@0: 
clasohm@0: MAKE-ALL (NJ 0.93) ran perfectly.  It took 4:05 hours!
clasohm@0: MAKE-ALL (Poly/ML) ran perfectly.  It took 3:31 hours!
clasohm@0: 
clasohm@0: **** New tar file placed on /homes/lcp (576K) **** 
clasohm@0: 
clasohm@0: **** Installation of Discrimination Nets ****
clasohm@0: 
clasohm@0: *Affected files (those mentioning Stringtree, compat_thms or rtr_resolve_tac)
clasohm@0: Pure/ROOT.ML,goals.ML,stringtree.ML,tactic.ML
clasohm@0: Provers/simp.ML
clasohm@0: HOL/ex/meson.ML
clasohm@0: 
clasohm@0: *Affected files (those mentioning compat_resolve_tac)
clasohm@0: Pure/tactic.ML
clasohm@0: Provers/typedsimp.ML
clasohm@0: CTT/ctt.ML
clasohm@0: 
clasohm@0: Pure/stringtree: saved on Isabelle/old
clasohm@0: Pure/net: new
clasohm@0: Pure/Makefile/FILES: now mentions net.ML, not stringtree.ML
clasohm@0: Pure/ROOT: now mentions net.ML, not stringtree.ML
clasohm@0: 
clasohm@0: Pure/goals/compat_goal: DELETED
clasohm@0: 
clasohm@0: Pure/tactic/compat_thms,rtr_resolve_tac,compat_resolve_tac,insert_thm,
clasohm@0: delete_thm,head_string: DELETED
clasohm@0: 
clasohm@0: Pure/tactic/biresolve_from_nets_tac, bimatch_from_nets_tac,
clasohm@0: net_biresolve_tac, net_bimatch_tac, resolve_from_net_tac, match_from_net_tac,
clasohm@0: net_resolve_tac, net_match_tac: NEW
clasohm@0: 
clasohm@0: Pure/tactic/filt_resolve_tac: new implementation using nets!
clasohm@0: 
clasohm@0: Provers/simp: replaced by new version
clasohm@0: 
clasohm@0: Provers/typedsimp: changed compat_resolve_tac to filt_resolve_tac and
clasohm@0: updated comments
clasohm@0: 
clasohm@0: CTT/ctt.ML: changed compat_resolve_tac to filt_resolve_tac 
clasohm@0: ZF/simpdata/typechk_step_tac: changed compat_resolve_tac to filt_resolve_tac
clasohm@0: 
clasohm@0: CTT tested
clasohm@0: 
clasohm@0: HOL/ex/meson/ins_term,has_reps: replaced Stringtree by Net
clasohm@0: 
clasohm@0: FOL tested
clasohm@0: 
clasohm@0: Provers/simp/cong_const: new, replaces head_string call in cong_consts
clasohm@0: Provers/simp: renamed variables: atomic to at and cong_consts to ccs
clasohm@0: 
clasohm@0: ZF/ex/bin/integ_of_bin_type: proof required reordering of rules --
clasohm@0: typechk_tac now respects this ordering!
clasohm@0: 
clasohm@0: ZF tested
clasohm@0: 
clasohm@0: DOCUMENTATION
clasohm@0: 
clasohm@0: Logics/CTT: Removed mention of compat_resolve_tac 
clasohm@0: Ref/goals: deleted compat_goal's entry
clasohm@0: 
clasohm@0: Provers/hypsubst/lasthyp_subst_tac: deleted
clasohm@0: 
clasohm@0: FOLP/ROOT/dest_eq: corrected; now hyp_subst_tac works!
clasohm@0: 
clasohm@0: 12 April
clasohm@0: 
clasohm@0: MAKE-ALL (NJ 0.93) ran perfectly.  It took 4:03 hours!
clasohm@0: MAKE-ALL (Poly/ML) ran perfectly.  It took 3:28 hours!
clasohm@0: 
clasohm@0: FOLP/{int-prover,classical}/safe_step_tac: uses eq_assume_tac, not assume_tac
clasohm@0: FOLP/{int-prover,classical}/inst_step_tac: restored, calls assume and mp_tac
clasohm@0: FOLP/{int-prover,classical}/step_tac: calls inst_step_tac 
clasohm@0: 
clasohm@0: {FOL,FOLP}/int-prover/safe_brls: removed (asm_rl,true) since assume_tac is
clasohm@0: used explicitly!!
clasohm@0: 
clasohm@0: FOLP/ifolp/uniq_assume_tac: new, since eq_assume_tac is almost useless
clasohm@0: 
clasohm@0: FOLP/{int-prover,classical}/uniq_mp_tac: replace eq_mp_tac and call
clasohm@0: uniq_assume_tac
clasohm@0: 
clasohm@0: Provers/classical: REPLACED BY 'NET' VERSION!
clasohm@0: 
clasohm@0: 13 April
clasohm@0: 
clasohm@0: MAKE-ALL (Poly/ML) failed in ZF and ran out of quota for Cube.
clasohm@0: 
clasohm@0: Unification bug (nothing to do with pattern unification)
clasohm@0: Cleaning of flex-flex pairs attempts to remove all occurrences of bound
clasohm@0: variables not common to both sides.  Arguments containing "banned" bound
clasohm@0: variables are deleted -- but this should ONLY be done if the occurrence is
clasohm@0: rigid!
clasohm@0: 
clasohm@0: unify/CHANGE_FAIL: new, for flexible occurrence of bound variable
clasohm@0: unify/change_bnos: now takes "flex" as argument, indicating path status
clasohm@0: 
clasohm@0: 14 April
clasohm@0: 
clasohm@0: MAKE-ALL (Poly/ML) failed in HOL (ASM_SIMP_TAC redefined!) and LK
clasohm@0: 
clasohm@0: LK/ex/hard-quant/37: added "by flexflex_tac" to compensate for flexflex
clasohm@0: changes
clasohm@0: 
clasohm@0: Pure/goals/gethyps: now calls METAHYPS directly
clasohm@0: 
clasohm@0: rm-logfiles: no longer mentions directories.  WAS
clasohm@0:     rm log {Pure,FOL,ZF,LCF,CTT,LK,Modal,HOL,Cube}/make*.log
clasohm@0:     rm {FOL,ZF,LCF,CTT,LK,Modal,HOL,Cube}/test
clasohm@0:     rm {FOL,ZF,LCF,CTT,LK,Modal,HOL,Cube}/.*.thy.ML
clasohm@0:     rm {FOL,ZF,HOL}/ex/.*.thy.ML
clasohm@0: 
clasohm@0: MAKE-ALL (Poly/ML) ran perfectly.  It took 2:39 hours! (albatross)
clasohm@0: 
clasohm@0: New version of simp on Isabelle/new -- instantiates unknowns provided only
clasohm@0: one rule may do so [SINCE REJECTED DUE TO UNPREDICTABLE BEHAVIOR]
clasohm@0: 
clasohm@0: works with FOLP/ex/nat, but in general could fail in the event of
clasohm@0: overlapping rewrite rules, since FOLP always instantiates unknowns during
clasohm@0: rewriting.
clasohm@0: 
clasohm@0: ZF: tested with new version
clasohm@0: 
clasohm@0: HOL: tested with new version, appeared to loop in llist/Lmap_ident
clasohm@0: 
clasohm@0: **** NEW VERSION OF ASM_SIMP_TAC, WITH METAHYPS ****
clasohm@0: 
clasohm@0: ZF: failed in perm/comp_mem_injD1: the rule anti_refl_rew is too ambiguous!
clasohm@0: ZF/wfrec: all uses of wf_ss' require
clasohm@0: by (METAHYPS (fn hyps => cut_facts_tac hyps 1 THEN
clasohm@0:                          SIMP_TAC (wf_ss' addrews (hyps)) 1) 1);
clasohm@0: 
clasohm@0: ZF/epsilon/eclose_least: changed ASM_SIMP_TAC to SIMP_TAC; this makes
clasohm@0: METAHYPS version work
clasohm@0: 
clasohm@0: ZF/arith/add_not_less_self: adds anti_refl_rew
clasohm@0: 
clasohm@0: ZF/ex/prop-log/hyps_finite: the use of UN_I is very bad -- too undirected.
clasohm@0: Swapping the premises of UN_I would probably allow instantiation.
clasohm@0: 
clasohm@0: ZF otherwise seems to work!
clasohm@0: 
clasohm@0: HOL/llist/llistE: loops! due to rewriting by Rep_LList_LCons of Vars
clasohm@0: 
clasohm@0: HOL/ex/prop-log/comp_lemma: failed due to uninstantiated Var in 
clasohm@0: (CCONTR_rule RS allI)
clasohm@0: 
clasohm@0: *** REJECTED
clasohm@0: 
clasohm@0: 15 April
clasohm@0: 
clasohm@0: These overnight runs involve Provers/simp.ML with old treatment of rules
clasohm@0: (match_tac) and no METAHYPS; they test the new flexflex pairs and
clasohm@0: discrimination nets, to see whether it runs faster.
clasohm@0: 
clasohm@0: MAKE-ALL (NJ 0.93) ran perfectly.  It took 3:39 hours (4 mins faster)
clasohm@0: MAKE-ALL (Poly/ML) ran perfectly.  It took 3:23 hours (5 mins faster)
clasohm@0: 
clasohm@0: ZF/simpdata/ZF_ss: deleted anti_refl_rew; non-linear patterns slow down
clasohm@0: discrimination nets (and this rewrite used only ONCE)
clasohm@0: 
clasohm@0: ZF/mem_not_refl: new; replaces obsolete anti_refl_rew
clasohm@0: 
clasohm@0: **Timing experiments**
clasohm@0: 
clasohm@0: fun HYP_SIMP_TAC ss = METAHYPS (fn hyps => HOL_SIMP_TAC (ss addrews hyps) 1);
clasohm@0: 
clasohm@0: On large examples such as ...
clasohm@0: HOL/arith/mod_quo_equality 
clasohm@0: HOL/llist/LListD_implies_ntrunc_equality
clasohm@0: ZF/ex/bin/integ_of_bin_succ
clasohm@0: ... it is 1.5 to 3 times faster than ASM_SIMP_TAC.  But cannot replace
clasohm@0: ASM_SIMP_TAC since the auto_tac sometimes fails due to lack of assumptions.
clasohm@0: If there are few assumptions then HYP_SIMP_TAC is no better.
clasohm@0: 
clasohm@0: Pure/Makefile: now copies $(ML_DBASE) to $(BIN)/Pure instead of calling
clasohm@0: make_database, so that users can call make_database for their object-logics.
clasohm@0: 
clasohm@0: Pure/tctical/SELECT_GOAL: now does nothing if i=1 and there is
clasohm@0: only one subgoal.
clasohm@0: 
clasohm@0: 19 April
clasohm@0: 
clasohm@0: MAKE-ALL (NJ 0.93) failed in HOL due to lack of disc space.
clasohm@0: MAKE-ALL (Poly/ML) ran perfectly.  It took 3:23 hours 
clasohm@0: 
clasohm@0: **** Installation of new simplifier ****
clasohm@0: 
clasohm@0: Provers/simp/EXEC: now calls METAHYPS and passes the hyps as an extra arg
clasohm@0: to the auto_tac.
clasohm@0: 
clasohm@0: FOL,HOL/simpdata: auto_tac now handles the hyps argument
clasohm@0: 
clasohm@0: ZF/simpdata/standard_auto_tac: deleted
clasohm@0: ZF/simpdata/auto_tac: added hyps argument
clasohm@0: ZF/epsilon/eclose_least_lemma: no special auto_tac 
clasohm@0: 
clasohm@0: */ex/ROOT: no longer use 'cd' commands; instead pathnames contain "ex/..."
clasohm@0: 
clasohm@0: 20 April
clasohm@0: 
clasohm@0: MAKE-ALL failed in HOL/Subst
clasohm@0: 
clasohm@0: HOL/Subst/setplus/cla_case: renamed imp_excluded_middle and simplified.
clasohm@0: Old version caused ambiguity in rewriting:
clasohm@0:      "[| P ==> P-->Q;  ~P ==> ~P-->Q |] ==> Q";
clasohm@0: 
clasohm@0: **** New tar file placed on /homes/lcp (????) **** 
clasohm@0: 
clasohm@0: Pure/Syntax: improvements to the printing of syntaxes
clasohm@0: Pure/Syntax/lexicon.ML: added name_of_token
clasohm@0: Pure/Syntax/earley0A.ML: updated print_gram
clasohm@0: 
clasohm@0: 21 April
clasohm@0: 
clasohm@0: MAKE-ALL (NJ 0.93) ran perfectly.  It took 3:44 hours
clasohm@0: MAKE-ALL (Poly/ML) failed in HOL due to lack of disc space
clasohm@0: 
clasohm@0: HOL/list,llist: now share NIL, CONS, List_Fun and List_case
clasohm@0: 
clasohm@0: make-all: now compresses the log files, which were taking up 4M; this
clasohm@0: reduces their space by more than 1/3
clasohm@0: 
clasohm@0: rm-logfiles: now deletes compressed log files.
clasohm@0: 
clasohm@0: ** Patrick Meche has noted that if the goal is stated with a leading !!
clasohm@0: quantifier, then the list of premises is always empty -- this gives the
clasohm@0: effect of an initial (cut_facts_tac prems 1).  The final theorem is the
clasohm@0: same as it would be without the quantifier.
clasohm@0: 
clasohm@0: ZF: used the point above to simplify many proofs
clasohm@0: ZF/domrange/cfast_tac: deleted, it simply called cut_facts_tac
clasohm@0: 
clasohm@0: 22 April
clasohm@0: 
clasohm@0: MAKE-ALL (NJ 0.93) ran perfectly.  It took 3:52 hours??
clasohm@0: MAKE-ALL (Poly/ML) ran perfectly.  It took 3:16 hours
clasohm@0: 
clasohm@0: 30 April
clasohm@0: 
clasohm@0: HOL: installation of finite set notation: {x1,...,xn} (by Tobias Nipkow)
clasohm@0: 
clasohm@0: HOL/set.thy,set.ML,fun.ML,equalities.ML: addition of rules for "insert",
clasohm@0: new derivations for "singleton"
clasohm@0: 
clasohm@0: HOL/llist.thy,llist.ML: changed {x.False} to {}
clasohm@0: 
clasohm@0: **** New tar file placed on /homes/lcp (584K) **** 
clasohm@0: 
clasohm@0: 4 May
clasohm@0: 
clasohm@0: MAKE-ALL (NJ 0.93) ran out of space in LK.
clasohm@0: MAKE-ALL (Poly/ML) ran perfectly.  It took 3:14 hours
clasohm@0: 
clasohm@0: Pure/Makefile: inserted "chmod u+w $(BIN)/Pure;" in case $(ML_DBASE) is
clasohm@0: write-protected
clasohm@0: 
clasohm@0: 5 May
clasohm@0: 
clasohm@0: HOL/list/not_Cons_self: renamed from l_not_Cons_l
clasohm@0: HOL/list/not_CONS_self: new
clasohm@0: 
clasohm@0: HOL/llist.thy/Lconst: changed type and def to remove Leaf
clasohm@0: HOL/llist.ML: changed Lconst theorems
clasohm@0: 
clasohm@0: 6 May
clasohm@0: 
clasohm@0: MAKE-ALL (Poly/ML) ran perfectly.  It took 3:18 hours
clasohm@0: 
clasohm@0: ** Installation of new HOL from Tobias **
clasohm@0: 
clasohm@0: HOL/ex/{finite,prop-log} made like the ZF versions
clasohm@0: HOL/hol.thy: type classes plus, minus, times; overloaded operators + - *
clasohm@0: HOL/set: set enumeration via "insert"
clasohm@0:          additions to set_cs and set_ss
clasohm@0: HOL/set,subset,equalities: various lemmas to do with {}, insert and -
clasohm@0: HOL/llist: One of the proofs needs one fewer commands
clasohm@0: HOL/arith: many proofs require type constraints due to overloading
clasohm@0: 
clasohm@0: ** end Installation **
clasohm@0: 
clasohm@0: ZF/ex/misc: added new lemmas from Abrial's paper
clasohm@0: 
clasohm@0: 7 May 
clasohm@0: 
clasohm@0: HOL/llist.ML/LList_corec_subset1: deleted a fast_tac call; the previous
clasohm@0: simplification now proves the subgoal.
clasohm@0: 
clasohm@0: **** New tar file placed on /homes/lcp (584K) **** 
clasohm@0: 
clasohm@0: ** Installation of new simplifier from Tobias **
clasohm@0: 
clasohm@0: The "case_splits" parameter of SimpFun is moved from the signature to the
clasohm@0: simpset.  SIMP_CASE_TAC and ASM_SIMP_CASE_TAC are removed.  The ordinary
clasohm@0: simplification tactics perform case splits if present in the simpset.
clasohm@0: 
clasohm@0: The simplifier finds out for itself what constant is affected.  Instead of
clasohm@0: supplying the pair (expand_if,"if"), supply just the rule expand_if.
clasohm@0: 
clasohm@0: This change affects all calls to SIMP_CASE_TAC and all applications of SimpFun.
clasohm@0: 
clasohm@0: MAKE-ALL (Poly/ML) ran perfectly.  It took 3:18 hours
clasohm@0: 
clasohm@0: Cube/ex: UNTIL1, UNTIL_THM: replaced by standard tactics DEPTH_SOLVE_1 and
clasohm@0: DEPTH_SOLVE
clasohm@0: 
clasohm@0: HOL: installation of NORM tag for simplication.  How was it forgotten??
clasohm@0: 
clasohm@0: HOL/hol.thy: declaration of NORM
clasohm@0: HOL/simpdata: NORM_def supplied to SimpFun
clasohm@0: 
clasohm@0: 10 May
clasohm@0: 
clasohm@0: MAKE-ALL (Poly/ML) ran perfectly.  It took 3:33 hours??
clasohm@0: 
clasohm@0: 11 May
clasohm@0: 
clasohm@0: HOL/prod/Prod_eq: renamed Pair_eq
clasohm@0: HOL/ex/lex-prod: wf_lex_prod: simplified proof
clasohm@0: 
clasohm@0: HOL/fun/inj_eq: new
clasohm@0: 
clasohm@0: HOL/llist/sumPairE: deleted, thanks to new simplifier's case splits!
clasohm@0: 
clasohm@0: 12 May
clasohm@0: 
clasohm@0: MAKE-ALL (NJ 0.93) ran out of space in HOL.
clasohm@0: MAKE-ALL (Poly/ML) failed in HOL.
clasohm@0: HOL/Subst/utermlemmas/utlemmas_ss: deleted Prod_eq from the congruence rules
clasohm@0: 
clasohm@0: 13 May
clasohm@0: 
clasohm@0: Pure/logic/flexpair: moved to term, with "equals" etc.  Now pervasive
clasohm@0: Pure/logic/mk_flexpair: now exported
clasohm@0: Pure/logic/dest_flexpair: new
clasohm@0: Pure/goals/print_exn: now prints the error message for TERM and TYPE
clasohm@0: 
clasohm@0: Pure/Syntax/sextension: now =?= has type ['a::{}, 'a] => prop because
clasohm@0: flexflex pairs can have any type at all.  Thus == must have the same type.
clasohm@0: 
clasohm@0: Pure/thm/flexpair_def: now =?= and == are equated for all 'a::{}.
clasohm@0: 
clasohm@0: Pure/tctical/equal_abs_elim,equal_abs_elim_list: new (for METAHYPS fix)
clasohm@0: Pure/tctical/METAHYPS: now works if new proof state has flexflex pairs
clasohm@0: 
clasohm@0: Pure/Syntax/earley0A,syntax,lexicon: Tokens are represented by strings now,
clasohm@0: not by integers.  (Changed by Tobias)
clasohm@0: 
clasohm@0: *** Installation of more printing functions ***
clasohm@0: 
clasohm@0: Pure/sign/sg: changed from a type abbrev to a datatype
clasohm@0: Pure/type/type_sig: changed from a type abbrev to a datatype
clasohm@0: These changes needed for abstract type printing in NJ
clasohm@0: 
clasohm@0: Pure/tctical/print_sg,print_theory: new
clasohm@0: 
clasohm@0: Pure/drule: new file containing derived rules and printing functions.
clasohm@0: Mostly from tctical.ML, but includes rewriting rules from tactic.ML.
clasohm@0: 
clasohm@0: Pure/ROOT: loads drule before tctical; TacticalFun,TacticFun,GoalsFun now
clasohm@0: depend on Drule and have sharing constraints.
clasohm@0: 
clasohm@0: 14 May
clasohm@0: 
clasohm@0: Installing new print functions for New Jersey: incompatible with Poly/ML!
clasohm@0: 
clasohm@0: Pure/NJ/install_pp_nj: new (requires datatypes as above)
clasohm@0: Pure/POLY/install_pp_nj: a dummy version
clasohm@0: 
clasohm@0: Pure/ROOT: calls install_pp_nj to install printing for NJ
clasohm@0: 
clasohm@0: */ROOT: added extra install_pp calls (sg, theory, cterm, typ, ctyp) for
clasohm@0: Poly/ML [ZF,LCF,Modal do not need them since they inherit them from another
clasohm@0: logic -- make_database is not used]
clasohm@0: 
clasohm@0: 17 May
clasohm@0: 
clasohm@0: MAKE-ALL (NJ 0.93) ran perfectly.  It took 3:57 hours??
clasohm@0: 
clasohm@0: Pure/Syntax/lexicon: Yet another leaner and faster version ... (from Tobias)
clasohm@0: 
clasohm@0: 18 May
clasohm@0: 
clasohm@0: MAKE-ALL (Poly/ML) ran perfectly.  It took 3:36 hours
clasohm@0: 
clasohm@0: 19 May
clasohm@0: 
clasohm@0: ZF/equalities/Union_singleton,Inter_singleton: now refer to {b} instead of
clasohm@0: complex assumptions
clasohm@0: 
clasohm@0: 20 May
clasohm@0: 
clasohm@0: HOL/list: Tobias added the [x1,...,xn] notation and the functions hd, tl,
clasohm@0: null and list_case.
clasohm@0: 
clasohm@0: 1 June
clasohm@0: 
clasohm@0: MAKE-ALL (Poly/ML) ran perfectly.  It took 3:39 hours
clasohm@0: 
clasohm@0: **** New tar file 92.tar.z placed on /homes/lcp (376K) **** 
clasohm@0: 
clasohm@0: MAKE-ALL (NJ 0.93) ran perfectly.  It took 1:49 hours on albatross.
clasohm@0: 
clasohm@0: Pure/tactic/dres_inst_tac,forw_inst_tac: now call the new
clasohm@0: make_elim_preserve to preserve Var indexes when creating the elimination
clasohm@0: rule.
clasohm@0: 
clasohm@0: ZF/ex/ramsey: modified calls to dres_inst_tac
clasohm@0: 
clasohm@0: 2 June
clasohm@0: 
clasohm@0: Pure/Thy/read/read_thy,use_thy: the .thy.ML file is now written to the
clasohm@0: current directory, since the pathname may lead to a non-writeable area.
clasohm@0: 
clasohm@0: HOL/arith: renamed / and // to div and mod
clasohm@0: ZF/arith: renamed #/ and #// to div and mod
clasohm@0: 
clasohm@0: MAKE-ALL (Poly/ML) ran perfectly.  It took 1:48 hours on albatross.
clasohm@0: 
clasohm@0: **** New tar file 92.tar.z placed on /homes/lcp (376K) **** 
clasohm@0: 
clasohm@0: Pure/NJ/commit: new dummy function
clasohm@0: FOLP/ex/ROOT: inserted commit call to avoid Poly/ML problems
clasohm@0: 
clasohm@0: make-all: now builds FOLP also!
clasohm@0: 
clasohm@0: 3 June
clasohm@0: 
clasohm@0: ZF/zf.thy,HOL/list.thy,HOL/set.thy: now constructions involving {_}, [_],
clasohm@0: <_,_> are formatted as {(_)}, [(_)], 
clasohm@0: 
clasohm@0: MAKE-ALL (Poly/ML) ran perfectly.  It took 4:37 hours on muscovy (with FOLP).
clasohm@0: 
clasohm@0: ZF/Makefile: removed obsolete target for .rules.ML
clasohm@0: 
clasohm@0: All object-logic Makefiles: EXAMPLES ARE NO LONGER SAVED.  This saves disc
clasohm@0: and avoids problems (in New Jersey ML) of writing to the currently
clasohm@0: executing image.
clasohm@0: 
clasohm@0: 4 June
clasohm@0: 
clasohm@0: Pure/logic/rewritec: now uses nets for greater speed.  Functor LogicFun now
clasohm@0: takes Net as argument.
clasohm@0: 
clasohm@0: Pure/ROOT: now loads net before logic.
clasohm@0: 
clasohm@0: MAKE-ALL (Poly/ML) failed in ZF and HOL.
clasohm@0: 
clasohm@0: LK/lk.thy: changed constant "not" to "Not" (for consistency with FOL)
clasohm@0: 
clasohm@0: 7 June
clasohm@0: 
clasohm@0: Pure/tactic/is_letdig: moved to library
clasohm@0: Pure/Syntax/lexicon/is_qld: deleted, was same as is_letdig
clasohm@0: 
clasohm@0: MAKE-ALL (Poly/ML) ran perfectly.  It took 2:07 hours on albatross.
clasohm@0: MAKE-ALL (NJ 0.93) ran perfectly.  It took 4:41 hours on dunlin.
clasohm@0: 
clasohm@0: HOL/set/UN1,INT1: new union/intersection operators.  Binders UN x.B(x),
clasohm@0: INT x.B(x).
clasohm@0: 
clasohm@0: HOL/univ,llist: now use UN x.B(x) instead of Union(range(B))
clasohm@0: 
clasohm@0: HOL/subset: added lattice properties for INT, UN (both forms)
clasohm@0: 
clasohm@0: 8 June
clasohm@0: 
clasohm@0: MAKE-ALL (NJ 0.93) ran perfectly.  It took 4:45 hours on dunlin.
clasohm@0: 
clasohm@0: **** New tar file 92.tar.z placed on /homes/lcp (384K) **** 
clasohm@0: 
clasohm@0: 14 June
clasohm@0: 
clasohm@0: HOL/list.thy/List_rec_def: changed pred_sexp (a variable!) to pred_Sexp.
clasohm@0: Using def_wfrec hides such errors!!
clasohm@0: 
clasohm@0: **** New tar file 92.tar.gz placed on /homes/lcp (384K) **** 
clasohm@0: 
clasohm@0: ** NEW VERSION FROM MUNICH WITH ==-REWRITING **
clasohm@0: 
clasohm@0: ** The following changes are Toby's **
clasohm@0: 
clasohm@0: type.ML:
clasohm@0: 
clasohm@0: Renamed mark_free to freeze_vars and thaw_tvars to thaw_vars.
clasohm@0: Added both functions to the signature.
clasohm@0: 
clasohm@0: sign.ML:
clasohm@0: 
clasohm@0: Added val subsig: sg * sg -> bool to signature.
clasohm@0: Added trueprop :: prop and mark_prop : prop => prop to pure_sg.
clasohm@0: 
clasohm@0: Added
clasohm@0: 
clasohm@0: val freeze_vars: term -> term
clasohm@0: val thaw_vars: term -> term
clasohm@0: val strip_all_imp: term * int -> term list * term * int
clasohm@0: 
clasohm@0: Moved rewritec_bottom and rewritec_top to thm.ML.
clasohm@0: Only bottom-up rewriting supported any longer.
clasohm@0: 
clasohm@0: thm.ML:
clasohm@0: 
clasohm@0: Added
clasohm@0: 
clasohm@0: (* internal form of conditional ==-rewrite rules *)
clasohm@0: type meta_simpset
clasohm@0: val add_mss: meta_simpset * thm list -> meta_simpset
clasohm@0: val empty_mss: meta_simpset
clasohm@0: val mk_mss: thm list -> meta_simpset
clasohm@0: 
clasohm@0: val mark_prop_def: thm
clasohm@0: val truepropI: thm
clasohm@0: val trueprop_def: thm
clasohm@0: 
clasohm@0: (* bottom-up conditional ==-rewriting with local ==>-assumptions *)
clasohm@0: val rewrite_cterm: meta_simpset -> (thm -> thm list)
clasohm@0:                    -> (meta_simpset -> thm list -> Sign.cterm -> thm)
clasohm@0:                    -> Sign.cterm -> thm
clasohm@0: val trace_simp: bool ref
clasohm@0: 
clasohm@0: Simplified concl_of: call to Logic.skip_flexpairs redundant.
clasohm@0: 
clasohm@0: drule.ML:
clasohm@0: 
clasohm@0: Added
clasohm@0: 
clasohm@0: (* rewriting *)
clasohm@0: val asm_rewrite_rule: (thm -> thm list) -> thm list -> thm -> thm
clasohm@0: val rewrite_goal_rule: (thm -> thm list) -> thm list -> int -> thm -> thm
clasohm@0: val rewrite_goals_rule: (thm -> thm list) -> thm list -> thm -> thm
clasohm@0: 
clasohm@0: (* derived concepts *)
clasohm@0: val forall_trueprop_eq: thm
clasohm@0: val implies_trueprop_eq: thm
clasohm@0: val mk_trueprop_eq: thm -> thm
clasohm@0: val reflexive_eq: thm
clasohm@0: val reflexive_thm: thm
clasohm@0: val trueprop_implies_eq: thm
clasohm@0: val thm_implies: thm -> thm -> thm
clasohm@0: val thm_equals: thm -> thm -> thm
clasohm@0: 
clasohm@0: (*Moved here from tactic.ML:*)
clasohm@0: val asm_rl: thm
clasohm@0: val cut_rl: thm
clasohm@0: val revcut_rl: thm
clasohm@0: 
clasohm@0: tactic.ML:
clasohm@0: 
clasohm@0: Added
clasohm@0: 
clasohm@0: val asm_rewrite_goal_tac: (thm -> thm list) -> thm list -> int -> tactic
clasohm@0: val asm_rewrite_goals_tac: (thm -> thm list) -> thm list -> tactic
clasohm@0: val asm_rewrite_tac: (thm -> thm list) -> thm list -> tactic
clasohm@0: val fold_goal_tac: thm list -> int -> tactic
clasohm@0: val rewrite_goal_tac: thm list -> int -> tactic
clasohm@0: 
clasohm@0: Moved to drule.ML:
clasohm@0: val asm_rl: thm
clasohm@0: val cut_rl: thm
clasohm@0: val revcut_rl: thm
clasohm@0: 
clasohm@0: goals.ML:
clasohm@0: 
clasohm@0: Changed prepare_proof to make sure that rewriting with empty list of
clasohm@0: meta-thms is identity.
clasohm@0: 
clasohm@0: ** End of Toby's changes **
clasohm@0: 
clasohm@0: 16 June
clasohm@0: 
clasohm@0: Pure/sign/typ_of,read_ctyp: new
clasohm@0: Pure/logic/dest_flexpair: now exported
clasohm@0: 
clasohm@0: Pure/drule/flexpair_intr,flexpair_elim: new; fixes a bug in
clasohm@0: flexpair_abs_elim_list
clasohm@0: 
clasohm@0: HOL/equalities/image_empty,image_insert: new
clasohm@0: HOL/ex/finite/Fin_imageI: new
clasohm@0: 
clasohm@0: Installed Martin Coen's CCL as new object-logic
clasohm@0: 
clasohm@0: 17 June
clasohm@0: 
clasohm@0: ** More changes from Munich (Markus Wenzel) **
clasohm@0: 
clasohm@0: Pure/library: added the, is_some, is_none, separate and improved space_implode
clasohm@0: Pure/sign: Sign.extend now calls Syntax.extend with list of constants
clasohm@0: Pure/symtab: added is_null
clasohm@0: Pure/Syntax/sextension: added empty_sext
clasohm@0: Pure/Syntax/syntax: changed Syntax.extend for compatibility with future version
clasohm@0: 
clasohm@0: HOL now exceeds poly's default heap size. Hence HOL/Makefile needs to
clasohm@0: specify -h 8000.
clasohm@0: 
clasohm@0: HOL/univ/ntrunc_subsetD, etc: deleted the useless j<k assumption
clasohm@0: 
clasohm@0: 18 June
clasohm@0: 
clasohm@0: MAKE-ALL (Poly/ML) ran perfectly.  It took 4:59 hours on dunlin (with CCL).
clasohm@0: 
clasohm@0: Pure/sign/read_def_cterm: now prints the offending terms, as well as the
clasohm@0: types, when exception TYPE is raised.
clasohm@0: 
clasohm@0: HOL/llist: some tidying
clasohm@0: 
clasohm@0: 23 June
clasohm@0: 
clasohm@0: HOL/llist/Lconst_type: generalized from Lconst(M): LList({M})
clasohm@0: 
clasohm@0: 24 June
clasohm@0: 
clasohm@0: MAKE-ALL (Poly/ML) ran perfectly.  It took 2:23 hours on albatross (with CCL)
clasohm@0: 
clasohm@0: MAKE-ALL (NJ 0.93) failed in CCL due to use of "abstraction" as an
clasohm@0: identifier in CCL.ML
clasohm@0: 
clasohm@0: **** New tar file 92.tar.gz placed on /homes/lcp (384K) **** (with CCL)
clasohm@0: 
clasohm@0: CCL/ROOT: added ".ML" extension to use commands for NJ compatibility
clasohm@0: 
clasohm@0: 25 June
clasohm@0: 
clasohm@0: MAKE-ALL (Poly/ML) ran perfectly.  It took 2:23 hours on albatross.
clasohm@0: MAKE-ALL (NJ 0.93) failed in HOL due to lack of ".ML" extension
clasohm@0: 
clasohm@0: HOL/fun/rangeE,imageE: eta-expanded f to get variable name preservation
clasohm@0: 
clasohm@0: HOL/llist/iterates_equality,lmap_lappend_distrib: tidied
clasohm@0: 
clasohm@0: 28 June
clasohm@0: 
clasohm@0: HOL/set/UN1_I: made the Var and Bound variables agree ("x") to get variable
clasohm@0: name preservation 
clasohm@0: 
clasohm@0: HOL/llist: co-induction rules applied with res_inst_tac to state the
clasohm@0: bisimulation directly
clasohm@0: 
clasohm@0: 2 July
clasohm@0: 
clasohm@0: MAKE-ALL (NJ 0.93) ran perfectly.  It took 2:10 hours on albatross.
clasohm@0: MAKE-ALL (Poly/ML) ran perfectly.  It took 2:23 hours on albatross.
clasohm@0: 
clasohm@0: 92/Makefile/$(BIN)/Pure: changed echo makefile= to echo database=
clasohm@0: 
clasohm@0: **** New tar file 92.tar.gz placed on /homes/lcp (424K) **** (with CCL)
clasohm@0: 
clasohm@0: 
clasohm@0: ** NEW VERSION FROM MUNICH WITH ABSTRACT SYNTAX TREES & NEW PARSER **
clasohm@0: 
clasohm@0: I have merged in the changes shown above since 24 June
clasohm@0: 
clasohm@0: CHANGES LOG OF Markus Wenzel (MMW)
clasohm@0: =======
clasohm@0: 
clasohm@0: 29-Jun-1993 MMW
clasohm@0:   *** Beta release of new syntax module ***
clasohm@0:   (should be 99% backwards compatible)
clasohm@0: 
clasohm@0:   Pure/Thy/ROOT.ML
clasohm@0:     added keywords for "translations" section
clasohm@0: 
clasohm@0:   Pure/Thy/syntax.ML
clasohm@0:     minor cleanup
clasohm@0:     added syntax for "translations" section
clasohm@0:     .*.thy.ML files now human readable
clasohm@0:     .*.thy.ML used to be generated incorrectly if no mixfix but "ML" section
clasohm@0:     "ML" section no longer demands any definitions (parse_translation, ...)
clasohm@0: 
clasohm@0:   Pure/Thy/read.ML
clasohm@0:     read_thy: added close_in
clasohm@0:     added file_exists (not perfect)
clasohm@0:     use_thy: now uses file_exists
clasohm@0: 
clasohm@0:   Pure/thm.ML
clasohm@0:     added syn_of: theory -> syntax
clasohm@0: 
clasohm@0:   Pure/Makefile
clasohm@0:     SYNTAX_FILES: added Syntax/ast.ML
clasohm@0: 
clasohm@0:   Pure/Syntax/pretty.ML
clasohm@0:     added str_of: T -> string
clasohm@0: 
clasohm@0:   Pure/Syntax/ast.ML
clasohm@0:     added this file
clasohm@0: 
clasohm@0:   Pure/Syntax/extension.ML
clasohm@0:   Pure/Syntax/parse_tree.ML
clasohm@0:   Pure/Syntax/printer.ML
clasohm@0:   Pure/Syntax/ROOT.ML
clasohm@0:   Pure/Syntax/sextension.ML
clasohm@0:   Pure/Syntax/syntax.ML
clasohm@0:   Pure/Syntax/type_ext.ML
clasohm@0:   Pure/Syntax/xgram.ML
clasohm@0:     These files have been completely rewritten, though the global structure
clasohm@0:     is similar to the old one.
clasohm@0: 
clasohm@0: 
clasohm@0: 30-Jun-1993 MMW
clasohm@0:   New versions of HOL and Cube: use translation rules wherever possible;
clasohm@0: 
clasohm@0:   HOL/hol.thy
clasohm@0:     cleaned up
clasohm@0:     removed alt_tr', mk_bindopt_tr'
clasohm@0:     alternative binders now implemented via translation rules and mk_alt_ast_tr'
clasohm@0: 
clasohm@0:   HOL/set.thy
clasohm@0:     cleaned up
clasohm@0:     removed type "finset"
clasohm@0:     now uses category "args" for finite sets
clasohm@0:     junked "ML" section
clasohm@0:     added "translations" section
clasohm@0: 
clasohm@0:   HOL/list.thy
clasohm@0:     cleaned up
clasohm@0:     removed type "listenum"
clasohm@0:     now uses category "args" for lists
clasohm@0:     junked "ML" section
clasohm@0:     added "translations" section
clasohm@0: 
clasohm@0:   Cube/cube.thy
clasohm@0:     cleaned up
clasohm@0:     changed indentation of Lam and Pi from 2 to 3
clasohm@0:     removed qnt_tr, qnt_tr', no_asms_tr, no_asms_tr'
clasohm@0:     fixed fun_tr': all but one newly introduced frees will have type dummyT
clasohm@0:     added "translations" section
clasohm@0: 
clasohm@0: 
clasohm@0: 30-Jun-1993, 05-Jul-1993 MMW
clasohm@0:   Improved toplevel pretty printers:
clasohm@0:     - unified interface for POLY and NJ;
clasohm@0:     - print functions now insert atomic string into the toplevel's pp stream,
clasohm@0:       rather than writing it to std_out (advantage: output appears at the
clasohm@0:       correct position, disadvantage: output cannot be broken);
clasohm@0:   (Is there anybody in this universe who exactly knows how Poly's install_pp
clasohm@0:   is supposed to work?);
clasohm@0: 
clasohm@0:   Pure/NJ.ML
clasohm@0:     removed dummy install_pp
clasohm@0:     added make_pp, install_pp
clasohm@0: 
clasohm@0:   Pure/POLY.ML
clasohm@0:     removed dummy install_pp_nj
clasohm@0:     added make_pp
clasohm@0: 
clasohm@0:   Pure/ROOT.ML
clasohm@0:     removed install_pp_nj stuff
clasohm@0: 
clasohm@0:   Pure/drule.ML
clasohm@0:     added str_of_sg, str_of_theory, str_of_thm
clasohm@0: 
clasohm@0:   Pure/install_pp.ML
clasohm@0:     added this file
clasohm@0: 
clasohm@0:   Pure/sign.ML
clasohm@0:     added str_of_term, str_of_typ, str_of_cterm, str_of_ctyp
clasohm@0: 
clasohm@0:   Pure/goals.ML
clasohm@0:     added str_of_term, str_of_typ
clasohm@0: 
clasohm@0:   CTT/ROOT.ML
clasohm@0:   Cube/ROOT.ML
clasohm@0:   FOL/ROOT.ML
clasohm@0:   FOLP/ROOT.ML
clasohm@0:   HOL/ROOT.ML
clasohm@0:   LK/ROOT.ML
clasohm@0:     replaced install_pp stuff by 'use "../Pure/install_pp.ML"'
clasohm@0: 
clasohm@0: 
clasohm@0: 01-Jul-1993 MMW
clasohm@0:   Misc small fixes
clasohm@0: 
clasohm@0:   CCL/ROOT.ML
clasohm@0:   HOL/ROOT.ML
clasohm@0:     added ".ML" suffix to some filenames
clasohm@0: 
clasohm@0:   HOL/ex/unsolved.ML
clasohm@0:     replaced HOL_Rule.thy by HOL.thy
clasohm@0: 
clasohm@0:   Pure/NJ.ML
clasohm@0:     quit was incorrectly int -> unit
clasohm@0: 
clasohm@0: END MMW CHANGES
clasohm@0: 
clasohm@0: Pure/Syntax/sextension/eta_contract: now initially false 
clasohm@0: 
clasohm@0: Pure/library/cat_lines: no longer calls "distinct"
clasohm@0: Pure/sign: replaced to calls of implode (map (apr(op^,"\n") o ... by cat_lines
clasohm@0: NB This could cause duplicate error messages from Pure/sign and Pure/type
clasohm@0: 
clasohm@0: Pure/goals/prove_goalw: now prints some of the information from print_exn
clasohm@0: 
clasohm@0: 9 July
clasohm@0: 
clasohm@0: MAKE-ALL (Poly/ML) ran perfectly.  It took 2:26 hours on albatross.
clasohm@0: 
clasohm@0: **** New tar file 93.tar.gz placed on /homes/lcp (480K) **** 
clasohm@0: 
clasohm@0: 12 July
clasohm@0: 
clasohm@0: MAKE-ALL (NJ 0.93) ran perfectly.  It took 2:13 hours on albatross.
clasohm@0: MAKE-ALL (Poly/ML) ran perfectly.  It took 2:25 hours on albatross.
clasohm@0: 
clasohm@0: 22 July
clasohm@0: 
clasohm@0: ZF/zf.thy: new version from Marcus Wenzel
clasohm@0: 
clasohm@0: ZF: ** installation of inductive definitions **
clasohm@0: 
clasohm@0: changing the argument order of "split"; affects fst/snd too
clasohm@0: sum.thy zf.thy ex/bin.thy ex/integ.thy ex/simult.thy ex/term.thy
clasohm@0: pair.ML  ex/integ.ML
clasohm@0: 
clasohm@0: changing the argument order of "case" and adding "Part": sum.thy sum.ML
clasohm@0: 
clasohm@0: ZF/zf.ML/rev_subsetD,rev_bspec: new
clasohm@0: 
clasohm@0: ZF/mono: new rules for implication
clasohm@0: ZF/mono/Collect_mono: now for use with implication rules
clasohm@0: 
clasohm@0: ZF/zf.ML/ballE': renamed rev_ballE
clasohm@0: 
clasohm@0: ZF/list.thy,list.ML: files renamed list-fn.thy, list-fn.ML
clasohm@0: ZF/list.ML: new version simply holds the datatype definition
clasohm@0: NB THE LIST CONSTRUCTORS ARE NOW Nil/Cons, not 0/Pair.
clasohm@0: 
clasohm@0: ZF/extend_ind.ML, datatype.ML: new files
clasohm@0: ZF/fin.ML: moved from ex/finite.ML
clasohm@0: 
clasohm@0: 23 July
clasohm@0: 
clasohm@0: ZF/ex/sexp: deleted this example -- it seems hardly worth the trouble of
clasohm@0: porting.
clasohm@0: 
clasohm@0: ZF/ex/bt.thy,bt.ML: files renamed bt-fn.thy, bt-fn.ML
clasohm@0: ZF/ex/bt.ML: new version simply holds the datatype definition
clasohm@0: 
clasohm@0: ZF/ex/term.thy,term.ML: files renamed term-fn.thy, term-fn.ML
clasohm@0: ZF/ex/term.ML: new version simply holds the datatype definition
clasohm@0: 
clasohm@0: ZF/sum/InlI,InrI: renamed from sum_InlI, sum_InlI
clasohm@0: 
clasohm@0: 26 July
clasohm@0: 
clasohm@0: ZF/univ/rank_ss: new, for proving recursion equations
clasohm@0: 
clasohm@0: ZF/domrange/image_iff,image_singleton_iff,vimage_iff,vimage_singleton_iff,
clasohm@0: field_of_prod:new
clasohm@0: 
clasohm@0: ZF/domrange/field_subset: modified
clasohm@0: 
clasohm@0: ZF/list/list_cases: no longer proved by induction!
clasohm@0: ZF/wf/wf_trancl: simplified proof
clasohm@0: 
clasohm@0: ZF/equalities: new laws for field
clasohm@0: 
clasohm@0: 29 July
clasohm@0: 
clasohm@0: ZF/trancl/trancl_induct: new
clasohm@0: ZF/trancl/rtrancl_induct,trancl_induct: now with more type information
clasohm@0: 
clasohm@0: ** More changes from Munich (Markus Wenzel) **
clasohm@0: 
clasohm@0: Update of new syntax module (aka macro system): mostly internal cleanup and
clasohm@0: polishing;
clasohm@0: 
clasohm@0:   Pure/Syntax/*
clasohm@0:     added Ast.stat_norm
clasohm@0:     added Syntax.print_gram, Syntax.print_trans, Syntax.print_syntax
clasohm@0:     cleaned type and Pure syntax: "_CLASSES" -> "classes", "_SORTS" -> "sorts",
clasohm@0:      "_==>" -> "==>", "_fun" -> "fun", added some space for printing
clasohm@0:     Printer: partial fix of the "PROP <aprop>" problem: print "PROP " before
clasohm@0:       any Var or Free of type propT
clasohm@0:     Syntax: added ndependent_tr, dependent_tr'
clasohm@0: 
clasohm@0:   Pure/sign.ML: removed declaration of "==>" (now in Syntax.pure_sext)
clasohm@0: 
clasohm@0: Changes to object logics: minor cleanups and replacement of most remaining ML
clasohm@0: translations by rewrite rules (see also file "Translations");
clasohm@0: 
clasohm@0:   ZF/zf.thy
clasohm@0:     added "translations" section
clasohm@0:     removed all parse/print translations except ndependent_tr, dependent_tr'
clasohm@0:     fixed dependent_tr': all but one newly introduced frees have type dummyT
clasohm@0:     replaced id by idt in order to make terms rereadable if !show_types
clasohm@0: 
clasohm@0:   Cube/cube.thy
clasohm@0:     removed necontext
clasohm@0:     replaced fun_tr/tr' by ndependent_tr/dependent_tr'
clasohm@0: 
clasohm@0:   CTT/ctt.thy
clasohm@0:     added translations rules for PROD and SUM
clasohm@0:     removed dependent_tr
clasohm@0:     removed definitions of ndependent_tr, dependent_tr'
clasohm@0: 
clasohm@0:   HOL/set.thy: replaced id by idt
clasohm@0: 
clasohm@0:   CCL/ROOT.ML: Logtic -> Logic
clasohm@0: 
clasohm@0:   CCL/set.thy
clasohm@0:     added "translations" section
clasohm@0:     removed "ML" section
clasohm@0:     replaced id by idt
clasohm@0: 
clasohm@0:   CCL/types.thy
clasohm@0:     added "translations" section
clasohm@0:     removed definitions of ndependent_tr, dependent_tr'
clasohm@0:     replaced id by idt
clasohm@0: 
clasohm@0: Yet another improvement of toplevel pretty printers: output now breakable;
clasohm@0: 
clasohm@0:   Pure/NJ.ML Pure/POLY.ML improved make_pp
clasohm@0: 
clasohm@0:   Pure/install_pp.ML: replaced str_of_* by pprint_*
clasohm@0: 
clasohm@0:   Pure/drule.ML: replaced str_of_{sg,theory,thm} by pprint_*
clasohm@0: 
clasohm@0:   Pure/sign.ML: replaced str_of_{term,typ,cterm,ctyp} by pprint_*
clasohm@0: 
clasohm@0:   Pure/goals.ML: fixed and replaced str_of_{term,typ} by pprint_*
clasohm@0: 
clasohm@0:   Pure/Syntax/pretty.ML: added pprint, quote
clasohm@0: 
clasohm@0: Minor changes and additions;
clasohm@0: 
clasohm@0:   Pure/sign.ML: renamed stamp "PURE" to "Pure"
clasohm@0: 
clasohm@0:   Pure/library.ML
clasohm@0:     added quote: string -> string
clasohm@0:     added to_lower: string -> bool
clasohm@0: 
clasohm@0:   Pure/NJ.ML,POLY.ML: added file_info of Carsten Clasohm
clasohm@0: 
clasohm@0: 30 July
clasohm@0: 
clasohm@0: MAKE-ALL (Poly/ML) ran perfectly.
clasohm@0: 
clasohm@0: Pure/goals/print_sign_exn: new, takes most code from print_exn
clasohm@0: Pure/goals/prove_goalw: displays exceptions using print_sign_exn
clasohm@0: 
clasohm@0: Pure/drule/print_sg: now calls pretty_sg to agree with pprint_sg
clasohm@0: 
clasohm@0: Pure/library,...: replaced front/nth_tail by take/drop.
clasohm@0: 
clasohm@0: Pure/term/typ_tfrees,typ_tvars,term_tfrees,term_tvars: new
clasohm@0: thm/mk_rew_triple, drule/types_sorts, sign/zero_tvar_indices: now use the above
clasohm@0: 
clasohm@0: Pure/logic/add_term_vars,add_term_frees,insert_aterm,atless:
clasohm@0: moved to term, joining similar functions for type variables;
clasohm@0: Logic.vars and Logic.frees are now term_vars and term_frees
clasohm@0: 
clasohm@0: Pure/term/subst_free: new
clasohm@0: 
clasohm@0: Pure/tactic/is_fact: newly exported
clasohm@0: 
clasohm@0: Provers/simp/mk_congs: uses filter_out is_fact to delete trivial cong rules
clasohm@0: 
clasohm@0: Pure/tactic/rename_last_tac: now uses Syntax.is_identifier instead of
clasohm@0: forall is_letdig
clasohm@0: 
clasohm@0: **** New tar file 93.tar.gz placed on /homes/lcp (448K) **** 
clasohm@0: 
clasohm@0: 2 August
clasohm@0: 
clasohm@0: MAKE-ALL (NJ 0.93) failed in ZF due to Compiler bug: elabDecl:open:FctBodyStr
clasohm@0: MAKE-ALL (Poly/ML) failed in ZF/enum.  It took 2:33 hours on albatross.
clasohm@0: 
clasohm@0: Pure/drule/triv_forall_equality: new
clasohm@0: Pure/tactic/prune_params_tac: new
clasohm@0: 
clasohm@0: Provers/hypsubst/bound_hyp_subst_tac: new, safer than hyp_subst_tac
clasohm@0: 
clasohm@0: 3 August
clasohm@0: 
clasohm@0: Pure/tactic/rule_by_tactic: new
clasohm@0: 
clasohm@0: ZF/perm/compEpair: now proved via rule_by_tactic
clasohm@0: 
clasohm@0: ZF/extend_ind/cases,mk_cases: new
clasohm@0: ZF/datatype/mk_free: new
clasohm@0: ZF/list: now calls List.mk_cases
clasohm@0: 
clasohm@0: 4 August
clasohm@0: 
clasohm@0: Provers/slow_tac,slow_best_tac: new
clasohm@0: 
clasohm@0: 5 August
clasohm@0: 
clasohm@0: MAKE-ALL (Poly/ML) failed in ZF
clasohm@0: 
clasohm@0: ZF/sum/sumE2: deleted since unused
clasohm@0: ZF/sum/sum_iff,sum_subset_iff,sum_equal_iff: new
clasohm@0: ZF/univ/Transset_Vfrom: new; used in proof of Transset_Vset
clasohm@0: 
clasohm@0: 6 August
clasohm@0: 
clasohm@0: Pure/goals/prepare_proof: after "Additional hypotheses", now actually
clasohm@0: prints them!
clasohm@0: 
clasohm@0: ZF/ordinal/Transset_Union_family, Transset_Inter_family: renamed from
clasohm@0: Transset_Union, Transset_Inter
clasohm@0: 
clasohm@0: ZF/ordinal/Transset_Union: new 
clasohm@0: ZF/univ/pair_in_univ: renamed Pair_in_univ
clasohm@0: 
clasohm@0: ZF/mono/product_mono: generalized to Sigma_mono; changed uses in trancl, univ
clasohm@0: 
clasohm@0: ZF/lfp/lfp_Tarski,def_lfp_Tarski: renamed from Tarski,def_Tarski; changed
clasohm@0: uses in extend_ind.ML, nat.ML, trancl.ML.
clasohm@0: 
clasohm@0: ZF/ex/misc: Schroeder-Bernstein Theorem moved here from lfp.ML
clasohm@0: 
clasohm@0: ZF/fixedpt.thy,.ML: renamed from lfp.thy,.ML, and gfp added
clasohm@0: 
clasohm@0: 9 August
clasohm@0: 
clasohm@0: ZF/zf.thy/ndependent_tr,dependent_tr': deleted, since they are now on
clasohm@0: Syntax/sextension. 
clasohm@0: 
clasohm@0: 11 August
clasohm@0: 
clasohm@0: Pure/library.ML: added functions
clasohm@0: assocs: (''a * 'b list) list -> ''a -> 'b list
clasohm@0: transitive_closure: (''a * ''a list) list -> (''a * ''a list) list
clasohm@0: 
clasohm@0: Pure/type.ML: deleted (inefficient) transitive_closure