edits.txt
changeset 0 a5a9c433f639
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/edits.txt	Thu Sep 16 12:20:38 1993 +0200
     1.3 @@ -0,0 +1,1372 @@
     1.4 +EDITS TO THE ISABELLE SYSTEM FOR 1993
     1.5 +
     1.6 +11 January 
     1.7 +
     1.8 +*/README: Eliminated references to Makefile.NJ, which no longer exists.
     1.9 +
    1.10 +**** New tar file placed on /homes/lcp (464K) **** 
    1.11 +
    1.12 +14 January
    1.13 +
    1.14 +Provers/simp/pr_goal_lhs: now distinct from pr_goal_concl so that tracing
    1.15 +prints conditions correctly.
    1.16 +
    1.17 +{CTT/arith,HOL/ex/arith/ZF/arith}/add_mult_distrib: renamed from
    1.18 +add_mult_dist, to agree with the other _distrib rules
    1.19 +
    1.20 +20 January
    1.21 +
    1.22 +Pure/Syntax/type_ext.ML: "I have fixed a few anomalies in the pretty
    1.23 +printing annotations for types.  Only the layout has changed." -- Toby
    1.24 +
    1.25 +21 January
    1.26 +
    1.27 +{CTT/arith,HOL/ex/arith/ZF/arith}/add_inverse_diff: renamed to add_diff_inverse
    1.28 +
    1.29 +22 January
    1.30 +
    1.31 +ZF/ex/equiv: new theory of equivalence classes
    1.32 +ZF/ex/integ: new theory of integers
    1.33 +HOL/set.thy: added indentation of 3 to all binding operators
    1.34 +
    1.35 +ZF/bool/boolI0,boolI1: renamed as bool_0I, bool_1I
    1.36 +
    1.37 +25 January
    1.38 +
    1.39 +MAKE-ALL (NJ 0.75) ran perfectly.  It took 3:19 hours!?
    1.40 +
    1.41 +ZF/bool/not,and,or,xor: new
    1.42 +
    1.43 +27 January
    1.44 +
    1.45 +ZF/ex/bin: new theory of binary integer arithmetic
    1.46 +
    1.47 +27 January
    1.48 +
    1.49 +MAKE-ALL (Poly/ML) ran perfectly.  It took 6:33 hours???
    1.50 +(ZF took almost 5 hours!)
    1.51 +
    1.52 +**** New tar file placed on /homes/lcp (472K) **** 
    1.53 +
    1.54 +HOL/set/UN_cong,INT_cong: new
    1.55 +HOL/subset/mem_rews,set_congs,set_ss: new
    1.56 +HOL/simpdata/o_apply: new; added to HOL_ss
    1.57 +
    1.58 +29 January
    1.59 +
    1.60 +Pure/Thy/syntax/mk_structure: the dummy theory created by type infixes is
    1.61 +now called name^"(type infix)" instead of "", avoid triggering a spurious
    1.62 +error "Attempt to merge different versions of theory: " in
    1.63 +Pure/sign/merge_stamps
    1.64 +
    1.65 +2 February
    1.66 +
    1.67 +MAKE-ALL (Poly/ML) ran perfectly.  It took 2:48 hours.  Runs in 1992 took
    1.68 +under 2:20 hours, but the new files in ZF/ex take time: nearly 23 minutes
    1.69 +according to make10836.log.
    1.70 +
    1.71 +Pure/Thy/scan/comment: renamed from komt
    1.72 +Pure/Thy/scan/numeric: renamed from zahl
    1.73 +
    1.74 +Pure/Syntax/syntax,lexicon,type_ext,extension,sextension: modified by
    1.75 +Tobias to change ID, TVAR, ... to lower case.
    1.76 +
    1.77 +Cube/cube.thy,HOL/hol.thy,HOL/set.thy,CTT/ctt.thy,LK/lk.thy,ZF/zf.thy: now
    1.78 +with ID, ... in lower case and other tidying
    1.79 +
    1.80 +3 February
    1.81 +
    1.82 +MAKE-ALL (Poly/ML) ran perfectly.  It took 2:50 hours.
    1.83 +
    1.84 +4 February
    1.85 +
    1.86 +HOL/nat/nat_ss: now includes the rule Suc_less_eq: (Suc(m) < Suc(n)) = (m<n)
    1.87 +and the nat_case rules and congruence rules
    1.88 +
    1.89 +HOL/sum/sumE: now has the "strong" form with equality assumptions.  WAS
    1.90 +    val prems = goalw Sum.thy [Inl_def,Inr_def]
    1.91 +	"[| !!x::'a. P(Inl(x));  !!y::'b. P(Inr(y)) \
    1.92 +    \    |] ==> P(s)";
    1.93 +    by (res_inst_tac [("t","s")] (Rep_Sum_inverse RS subst) 1);
    1.94 +    by (rtac (rewrite_rule [Sum_def] Rep_Sum RS CollectE) 1);
    1.95 +    by (REPEAT (eresolve_tac [disjE,exE,ssubst] 1 ORELSE resolve_tac prems 1));
    1.96 +    val sumE = result();
    1.97 +
    1.98 +8 February
    1.99 +
   1.100 +Changes from Tobias:
   1.101 +Pure/Thy/parse: now list_of admits the empty phrase, while listof_1 does not
   1.102 +Pure/Thy/syntax: uses new list_of, list_of1
   1.103 +
   1.104 +9 February
   1.105 +
   1.106 +HOL/ex/arith: moved to main HOL directory
   1.107 +HOL/prod: now define the type "unit" and constant "(): unit"
   1.108 +
   1.109 +11 February
   1.110 +
   1.111 +HOL/arith: eliminated redefinitions of nat_ss and arith_ss
   1.112 +
   1.113 +12 February
   1.114 +
   1.115 +MAKE-ALL (Poly/ML) ran perfectly.  It took 2:50 hours.
   1.116 +
   1.117 +Pure/Thy/scan/string: now correctly recognizes ML-style strings.
   1.118 +
   1.119 +15 February
   1.120 +
   1.121 +MAKE-ALL (NJ 0.75) ran perfectly.  It took 1:37 hours (on albatross)
   1.122 +MAKE-ALL (NJ 0.75) ran perfectly.  It took 2:42 hours (on dunlin)
   1.123 +MAKE-ALL (Poly/ML) ran perfectly.  It took 2:53 hours (on dunlin)
   1.124 +
   1.125 +**** New tar file placed on /homes/lcp (480K) **** 
   1.126 +
   1.127 +18 February
   1.128 +
   1.129 +Pure/Syntax/earley0A/compile_xgram: Tobias deleted the third argument, as
   1.130 +it was unused.
   1.131 +
   1.132 +Pure/Syntax/earley0A: modified accordingly.
   1.133 +
   1.134 +19 February
   1.135 +
   1.136 +MAKE-ALL (NJ 0.75) ran perfectly.  It took 3:37 hours 
   1.137 +MAKE-ALL (Poly/ML) ran perfectly.  It took 2:52 hours
   1.138 +
   1.139 +**** New tar file placed on /homes/lcp (480K) **** 
   1.140 +
   1.141 +20 February
   1.142 +
   1.143 +MAKE-ALL (NJ 0.93) ran perfectly.  It took 3:30 hours 
   1.144 +
   1.145 +10 March
   1.146 +
   1.147 +HOL/fun/image_eqI: fixed bad pattern
   1.148 +
   1.149 +11 March
   1.150 +
   1.151 +MAKE-ALL (Poly/ML) failed in HOL!
   1.152 +
   1.153 +HOL/fun: moved "mono" proofs to HOL/subset, since they rely on subset laws
   1.154 +of Int and Un.
   1.155 +
   1.156 +12 March
   1.157 +
   1.158 +ZF/ex/misc: new example from Bledsoe
   1.159 +
   1.160 +15 March
   1.161 +
   1.162 +ZF/perm: two new theorems inspired by Pastre
   1.163 +
   1.164 +16 March
   1.165 +
   1.166 +Weakened congruence rules for HOL: speeds simplification considerably by
   1.167 +NOT simplifying the body of a conditional or eliminator.
   1.168 +
   1.169 +HOL/simpdata/mk_weak_congs: new, to make weakened congruence rules
   1.170 +
   1.171 +HOL/simpdata/congs: renamed HOL_congs and weakened the "if" rule
   1.172 +
   1.173 +HOL/simpdata/HOL_congs: now contains polymorphic rules for the overloaded
   1.174 +operators < and <=
   1.175 +
   1.176 +HOL/prod: weakened the congruence rule for split
   1.177 +HOL/sum: weakened the congruence rule for case
   1.178 +HOL/nat: weakened the congruence rule for nat_case and nat_rec
   1.179 +HOL/list: weakened the congruence rule for List_rec and list_rec
   1.180 +
   1.181 +HOL & test rebuilt perfectly
   1.182 +
   1.183 +Pure/goals/prepare_proof/mkresult: fixed bug in signature check.  Now
   1.184 +compares the FINAL signature with that from the original theory.
   1.185 +
   1.186 +Pure/goals/prepare_proof: ensures that [prove_]goalw checks that the
   1.187 +definitions do not update the proof state.
   1.188 +
   1.189 +17 March
   1.190 +
   1.191 +MAKE-ALL (Poly/ML) ran perfectly.
   1.192 +
   1.193 +18 March
   1.194 +
   1.195 +MAKE-ALL (Poly/ML) failed in HOL/ex/Substitutions
   1.196 +
   1.197 +HOL/ex/Subst/setplus: changed Set.thy to Setplus.thy where
   1.198 +necessary
   1.199 +
   1.200 +ZF/perm: proved some rules about inj and surj
   1.201 +
   1.202 +ZF/ex/misc: did some of Pastre's examples
   1.203 +
   1.204 +Pure/library/gen_ins,gen_union: new
   1.205 +
   1.206 +HOL/ex/Subst/subst: renamed rangeE to srangeE
   1.207 +
   1.208 +18 March
   1.209 +
   1.210 +MAKE-ALL (Poly/ML) failed in HOL/ex/term due to renaming of list_ss in
   1.211 +ex/Subst/alist
   1.212 +
   1.213 +HOL/list/list_congs: new; re-organized simpsets a bit
   1.214 +
   1.215 +Pure/goals/sign_error: new
   1.216 +
   1.217 +Pure/goals/prepare_proof,by_com: now print the list of new theories when
   1.218 +the signature of the proof state changes 
   1.219 +
   1.220 +HOL/prod,sexp: renamed fst, snd to fst_conv, snd_conv to avoid over-writing
   1.221 +the library functions fst, snd
   1.222 +
   1.223 +HOL/fun/image_compose: new
   1.224 +
   1.225 +21 March
   1.226 +
   1.227 +MAKE-ALL (NJ 0.93) ran perfectly.  It took 3:50 hours 
   1.228 +MAKE-ALL (Poly/ML) ran perfectly.  It took 3:21 hours
   1.229 +Much slower now (about 30 minutes!) because of HOL/ex/Subst
   1.230 +
   1.231 +**** New tar file placed on /homes/lcp (504K) **** 
   1.232 +
   1.233 +ZF/pair,simpdata: renamed fst, snd to fst_conv, snd_conv to avoid over-writing
   1.234 +the library functions fst, snd
   1.235 +
   1.236 +HOL/prod/prod_fun_imageI,E: new
   1.237 +
   1.238 +HOL/ex/Subst/Unify: renamed to Unifier to avoid clobbering structure Unify
   1.239 +of Pure
   1.240 +
   1.241 +24 March
   1.242 +
   1.243 +HOL/trancl/comp_subset_Sigma: new
   1.244 +HOL/wf/wfI: new
   1.245 +
   1.246 +HOL/Subst: moved from HOL/ex/Subst to shorten pathnames
   1.247 +HOL/Makefile: target 'test' now loads Subst/ROOT separately
   1.248 +
   1.249 +*** Installation of gfp, coinduction, ... to HOL ***
   1.250 +
   1.251 +HOL/gfp,llist: new
   1.252 +HOL/univ,sexp,list: replaced with new version
   1.253 +
   1.254 +Sexp is now the set of all well-founded trees, each of type 'a node set.
   1.255 +There is no longer a type 'sexp'.  Initial algebras require more explicit
   1.256 +type checking than before.  Defining a type 'sexp' would eliminate this,
   1.257 +but would also require a whole new set of primitives, similar to those
   1.258 +defined in univ.thy but restricted to well-founded trees.
   1.259 +
   1.260 +25 March
   1.261 +
   1.262 +Pure/thm: renamed 'bires' to 'eres' in many places (not exported) --
   1.263 +biresolution now refers to resolution with (flag,rule) pairs.
   1.264 +
   1.265 +Pure/thm/bicompose_aux: SOUNDNESS BUG concerning variable renaming.  A Var in
   1.266 +a premise was getting renamed when its occurrence in the flexflex pairs was
   1.267 +not.  Martin Coen supplied the following proof of True=False in HOL:
   1.268 +
   1.269 +    val [prem] = goal Set.thy "EX a:{c}.p=a ==> p=c";
   1.270 +    br (prem RS bexE) 1; be ssubst 1; be singletonD 1;
   1.271 +    val l1 = result();
   1.272 +
   1.273 +    val rls = [refl] RL [bexI] RL [l1];
   1.274 +
   1.275 +    goal Set.thy "True = False";
   1.276 +    brs rls 1; br singletonI 1;
   1.277 +    result();
   1.278 +
   1.279 +Marcus Moore noted that the error only occurred with
   1.280 +Logic.auto_rename:=false.  Elements of the fix:
   1.281 +
   1.282 +1.  rename_bvs, rename_bvars and bicompose_aux/newAs take tpairs (the
   1.283 +existing flex-flex pairs) as an extra argument.  rename_bvs preserves all
   1.284 +Vars in tpairs.
   1.285 +
   1.286 +2.  bicompose_aux/tryasms and res now unpack the "cell" and supply its tpairs
   1.287 +to newAs.
   1.288 +
   1.289 +HOL/lfp,gfp,ex/set: renamed Tarski to lfp_Tarski
   1.290 +
   1.291 +HOL/lfp,list,llist,nat,sexp,trancl,Subst/uterm,ex/simult,ex/term: renamed
   1.292 +def_Tarski to def_lfp_Tarski 
   1.293 +
   1.294 +26 March
   1.295 +
   1.296 +MAKE-ALL (NJ 0.93) ran perfectly.  It took 4:25 hours!
   1.297 +MAKE-ALL (Poly/ML) ran perfectly.  It took 3:54 hours! (jobs overlapped)
   1.298 +
   1.299 +Pure/Thy/scan/is_digit,is_letter: deleted.  They are already in
   1.300 +Pure/library, and these versions used non-Standard string comparisons!
   1.301 +
   1.302 +Repairing a fault reported by David Aspinall:
   1.303 +  show_types := true;  read "a";  (* followed by  'prin it' for NJ *)
   1.304 +Raises exception  LIST "hd".   Also has the side effect of leaving
   1.305 +show_types set at false. 
   1.306 +
   1.307 +Pure/goals/read: no longer creates a null TVar
   1.308 +Pure/Syntax/lexicon/string_of_vname: now handles null names
   1.309 +Pure/Syntax/printer/string_of_typ: tidied
   1.310 +
   1.311 +/usr/groups/theory/isabelle/92/Pure/thm: replaced by new version to fix bug
   1.312 +MAKE-ALL on this directory ran perfectly
   1.313 +/usr/groups/theory/ml-aftp/Isabelle92.tar.Z: replaced by new version
   1.314 +
   1.315 +29 March
   1.316 +
   1.317 +MAKE-ALL (NJ 0.93) ran perfectly.  It took 4:14 hours!
   1.318 +MAKE-ALL (Poly/ML) ran perfectly.  It took 3:43 hours!
   1.319 +
   1.320 +**** New tar file placed on /homes/lcp (518K) **** 
   1.321 +
   1.322 +30 March
   1.323 +
   1.324 +ZF/univ/cons_in_Vfrom: deleted "[| a: Vfrom(A,i);  b<=Vfrom(A,i) |] ==>
   1.325 +cons(a,b) : Vfrom(A,succ(i))" since it was useless.
   1.326 +
   1.327 +8 April
   1.328 +
   1.329 +MAKE-ALL (Poly/ML) ran perfectly.  It took 3:49 hours!
   1.330 +
   1.331 +**** New tar file placed on /homes/lcp (520K) **** 
   1.332 +
   1.333 +**** Updates for pattern unification (Tobias Nipkow) ****
   1.334 +
   1.335 +Pure/pattern.ML: new, pattern unification
   1.336 +
   1.337 +Pure/Makefile and ROOT.ML: included pattern.ML
   1.338 +
   1.339 +Pure/library.ML: added predicate downto0
   1.340 +
   1.341 +Pure/unify.ML: call pattern unification first. Removed call to could_unify.
   1.342 +
   1.343 +FOL/Makefile/FILES: now mentions ifol.ML (previously repeated fol.ML instead)
   1.344 +
   1.345 +**** Installation of Martin Coen's FOLP (FOL + proof objects) ****
   1.346 +
   1.347 +renamed PFOL, PIFOL to FOLP, IFOLP, etc.
   1.348 +
   1.349 +9 April
   1.350 +
   1.351 +MAKE-ALL (NJ 0.93) ran perfectly.  It took 4:05 hours!
   1.352 +MAKE-ALL (Poly/ML) ran perfectly.  It took 3:31 hours!
   1.353 +
   1.354 +**** New tar file placed on /homes/lcp (576K) **** 
   1.355 +
   1.356 +**** Installation of Discrimination Nets ****
   1.357 +
   1.358 +*Affected files (those mentioning Stringtree, compat_thms or rtr_resolve_tac)
   1.359 +Pure/ROOT.ML,goals.ML,stringtree.ML,tactic.ML
   1.360 +Provers/simp.ML
   1.361 +HOL/ex/meson.ML
   1.362 +
   1.363 +*Affected files (those mentioning compat_resolve_tac)
   1.364 +Pure/tactic.ML
   1.365 +Provers/typedsimp.ML
   1.366 +CTT/ctt.ML
   1.367 +
   1.368 +Pure/stringtree: saved on Isabelle/old
   1.369 +Pure/net: new
   1.370 +Pure/Makefile/FILES: now mentions net.ML, not stringtree.ML
   1.371 +Pure/ROOT: now mentions net.ML, not stringtree.ML
   1.372 +
   1.373 +Pure/goals/compat_goal: DELETED
   1.374 +
   1.375 +Pure/tactic/compat_thms,rtr_resolve_tac,compat_resolve_tac,insert_thm,
   1.376 +delete_thm,head_string: DELETED
   1.377 +
   1.378 +Pure/tactic/biresolve_from_nets_tac, bimatch_from_nets_tac,
   1.379 +net_biresolve_tac, net_bimatch_tac, resolve_from_net_tac, match_from_net_tac,
   1.380 +net_resolve_tac, net_match_tac: NEW
   1.381 +
   1.382 +Pure/tactic/filt_resolve_tac: new implementation using nets!
   1.383 +
   1.384 +Provers/simp: replaced by new version
   1.385 +
   1.386 +Provers/typedsimp: changed compat_resolve_tac to filt_resolve_tac and
   1.387 +updated comments
   1.388 +
   1.389 +CTT/ctt.ML: changed compat_resolve_tac to filt_resolve_tac 
   1.390 +ZF/simpdata/typechk_step_tac: changed compat_resolve_tac to filt_resolve_tac
   1.391 +
   1.392 +CTT tested
   1.393 +
   1.394 +HOL/ex/meson/ins_term,has_reps: replaced Stringtree by Net
   1.395 +
   1.396 +FOL tested
   1.397 +
   1.398 +Provers/simp/cong_const: new, replaces head_string call in cong_consts
   1.399 +Provers/simp: renamed variables: atomic to at and cong_consts to ccs
   1.400 +
   1.401 +ZF/ex/bin/integ_of_bin_type: proof required reordering of rules --
   1.402 +typechk_tac now respects this ordering!
   1.403 +
   1.404 +ZF tested
   1.405 +
   1.406 +DOCUMENTATION
   1.407 +
   1.408 +Logics/CTT: Removed mention of compat_resolve_tac 
   1.409 +Ref/goals: deleted compat_goal's entry
   1.410 +
   1.411 +Provers/hypsubst/lasthyp_subst_tac: deleted
   1.412 +
   1.413 +FOLP/ROOT/dest_eq: corrected; now hyp_subst_tac works!
   1.414 +
   1.415 +12 April
   1.416 +
   1.417 +MAKE-ALL (NJ 0.93) ran perfectly.  It took 4:03 hours!
   1.418 +MAKE-ALL (Poly/ML) ran perfectly.  It took 3:28 hours!
   1.419 +
   1.420 +FOLP/{int-prover,classical}/safe_step_tac: uses eq_assume_tac, not assume_tac
   1.421 +FOLP/{int-prover,classical}/inst_step_tac: restored, calls assume and mp_tac
   1.422 +FOLP/{int-prover,classical}/step_tac: calls inst_step_tac 
   1.423 +
   1.424 +{FOL,FOLP}/int-prover/safe_brls: removed (asm_rl,true) since assume_tac is
   1.425 +used explicitly!!
   1.426 +
   1.427 +FOLP/ifolp/uniq_assume_tac: new, since eq_assume_tac is almost useless
   1.428 +
   1.429 +FOLP/{int-prover,classical}/uniq_mp_tac: replace eq_mp_tac and call
   1.430 +uniq_assume_tac
   1.431 +
   1.432 +Provers/classical: REPLACED BY 'NET' VERSION!
   1.433 +
   1.434 +13 April
   1.435 +
   1.436 +MAKE-ALL (Poly/ML) failed in ZF and ran out of quota for Cube.
   1.437 +
   1.438 +Unification bug (nothing to do with pattern unification)
   1.439 +Cleaning of flex-flex pairs attempts to remove all occurrences of bound
   1.440 +variables not common to both sides.  Arguments containing "banned" bound
   1.441 +variables are deleted -- but this should ONLY be done if the occurrence is
   1.442 +rigid!
   1.443 +
   1.444 +unify/CHANGE_FAIL: new, for flexible occurrence of bound variable
   1.445 +unify/change_bnos: now takes "flex" as argument, indicating path status
   1.446 +
   1.447 +14 April
   1.448 +
   1.449 +MAKE-ALL (Poly/ML) failed in HOL (ASM_SIMP_TAC redefined!) and LK
   1.450 +
   1.451 +LK/ex/hard-quant/37: added "by flexflex_tac" to compensate for flexflex
   1.452 +changes
   1.453 +
   1.454 +Pure/goals/gethyps: now calls METAHYPS directly
   1.455 +
   1.456 +rm-logfiles: no longer mentions directories.  WAS
   1.457 +    rm log {Pure,FOL,ZF,LCF,CTT,LK,Modal,HOL,Cube}/make*.log
   1.458 +    rm {FOL,ZF,LCF,CTT,LK,Modal,HOL,Cube}/test
   1.459 +    rm {FOL,ZF,LCF,CTT,LK,Modal,HOL,Cube}/.*.thy.ML
   1.460 +    rm {FOL,ZF,HOL}/ex/.*.thy.ML
   1.461 +
   1.462 +MAKE-ALL (Poly/ML) ran perfectly.  It took 2:39 hours! (albatross)
   1.463 +
   1.464 +New version of simp on Isabelle/new -- instantiates unknowns provided only
   1.465 +one rule may do so [SINCE REJECTED DUE TO UNPREDICTABLE BEHAVIOR]
   1.466 +
   1.467 +works with FOLP/ex/nat, but in general could fail in the event of
   1.468 +overlapping rewrite rules, since FOLP always instantiates unknowns during
   1.469 +rewriting.
   1.470 +
   1.471 +ZF: tested with new version
   1.472 +
   1.473 +HOL: tested with new version, appeared to loop in llist/Lmap_ident
   1.474 +
   1.475 +**** NEW VERSION OF ASM_SIMP_TAC, WITH METAHYPS ****
   1.476 +
   1.477 +ZF: failed in perm/comp_mem_injD1: the rule anti_refl_rew is too ambiguous!
   1.478 +ZF/wfrec: all uses of wf_ss' require
   1.479 +by (METAHYPS (fn hyps => cut_facts_tac hyps 1 THEN
   1.480 +                         SIMP_TAC (wf_ss' addrews (hyps)) 1) 1);
   1.481 +
   1.482 +ZF/epsilon/eclose_least: changed ASM_SIMP_TAC to SIMP_TAC; this makes
   1.483 +METAHYPS version work
   1.484 +
   1.485 +ZF/arith/add_not_less_self: adds anti_refl_rew
   1.486 +
   1.487 +ZF/ex/prop-log/hyps_finite: the use of UN_I is very bad -- too undirected.
   1.488 +Swapping the premises of UN_I would probably allow instantiation.
   1.489 +
   1.490 +ZF otherwise seems to work!
   1.491 +
   1.492 +HOL/llist/llistE: loops! due to rewriting by Rep_LList_LCons of Vars
   1.493 +
   1.494 +HOL/ex/prop-log/comp_lemma: failed due to uninstantiated Var in 
   1.495 +(CCONTR_rule RS allI)
   1.496 +
   1.497 +*** REJECTED
   1.498 +
   1.499 +15 April
   1.500 +
   1.501 +These overnight runs involve Provers/simp.ML with old treatment of rules
   1.502 +(match_tac) and no METAHYPS; they test the new flexflex pairs and
   1.503 +discrimination nets, to see whether it runs faster.
   1.504 +
   1.505 +MAKE-ALL (NJ 0.93) ran perfectly.  It took 3:39 hours (4 mins faster)
   1.506 +MAKE-ALL (Poly/ML) ran perfectly.  It took 3:23 hours (5 mins faster)
   1.507 +
   1.508 +ZF/simpdata/ZF_ss: deleted anti_refl_rew; non-linear patterns slow down
   1.509 +discrimination nets (and this rewrite used only ONCE)
   1.510 +
   1.511 +ZF/mem_not_refl: new; replaces obsolete anti_refl_rew
   1.512 +
   1.513 +**Timing experiments**
   1.514 +
   1.515 +fun HYP_SIMP_TAC ss = METAHYPS (fn hyps => HOL_SIMP_TAC (ss addrews hyps) 1);
   1.516 +
   1.517 +On large examples such as ...
   1.518 +HOL/arith/mod_quo_equality 
   1.519 +HOL/llist/LListD_implies_ntrunc_equality
   1.520 +ZF/ex/bin/integ_of_bin_succ
   1.521 +... it is 1.5 to 3 times faster than ASM_SIMP_TAC.  But cannot replace
   1.522 +ASM_SIMP_TAC since the auto_tac sometimes fails due to lack of assumptions.
   1.523 +If there are few assumptions then HYP_SIMP_TAC is no better.
   1.524 +
   1.525 +Pure/Makefile: now copies $(ML_DBASE) to $(BIN)/Pure instead of calling
   1.526 +make_database, so that users can call make_database for their object-logics.
   1.527 +
   1.528 +Pure/tctical/SELECT_GOAL: now does nothing if i=1 and there is
   1.529 +only one subgoal.
   1.530 +
   1.531 +19 April
   1.532 +
   1.533 +MAKE-ALL (NJ 0.93) failed in HOL due to lack of disc space.
   1.534 +MAKE-ALL (Poly/ML) ran perfectly.  It took 3:23 hours 
   1.535 +
   1.536 +**** Installation of new simplifier ****
   1.537 +
   1.538 +Provers/simp/EXEC: now calls METAHYPS and passes the hyps as an extra arg
   1.539 +to the auto_tac.
   1.540 +
   1.541 +FOL,HOL/simpdata: auto_tac now handles the hyps argument
   1.542 +
   1.543 +ZF/simpdata/standard_auto_tac: deleted
   1.544 +ZF/simpdata/auto_tac: added hyps argument
   1.545 +ZF/epsilon/eclose_least_lemma: no special auto_tac 
   1.546 +
   1.547 +*/ex/ROOT: no longer use 'cd' commands; instead pathnames contain "ex/..."
   1.548 +
   1.549 +20 April
   1.550 +
   1.551 +MAKE-ALL failed in HOL/Subst
   1.552 +
   1.553 +HOL/Subst/setplus/cla_case: renamed imp_excluded_middle and simplified.
   1.554 +Old version caused ambiguity in rewriting:
   1.555 +     "[| P ==> P-->Q;  ~P ==> ~P-->Q |] ==> Q";
   1.556 +
   1.557 +**** New tar file placed on /homes/lcp (????) **** 
   1.558 +
   1.559 +Pure/Syntax: improvements to the printing of syntaxes
   1.560 +Pure/Syntax/lexicon.ML: added name_of_token
   1.561 +Pure/Syntax/earley0A.ML: updated print_gram
   1.562 +
   1.563 +21 April
   1.564 +
   1.565 +MAKE-ALL (NJ 0.93) ran perfectly.  It took 3:44 hours
   1.566 +MAKE-ALL (Poly/ML) failed in HOL due to lack of disc space
   1.567 +
   1.568 +HOL/list,llist: now share NIL, CONS, List_Fun and List_case
   1.569 +
   1.570 +make-all: now compresses the log files, which were taking up 4M; this
   1.571 +reduces their space by more than 1/3
   1.572 +
   1.573 +rm-logfiles: now deletes compressed log files.
   1.574 +
   1.575 +** Patrick Meche has noted that if the goal is stated with a leading !!
   1.576 +quantifier, then the list of premises is always empty -- this gives the
   1.577 +effect of an initial (cut_facts_tac prems 1).  The final theorem is the
   1.578 +same as it would be without the quantifier.
   1.579 +
   1.580 +ZF: used the point above to simplify many proofs
   1.581 +ZF/domrange/cfast_tac: deleted, it simply called cut_facts_tac
   1.582 +
   1.583 +22 April
   1.584 +
   1.585 +MAKE-ALL (NJ 0.93) ran perfectly.  It took 3:52 hours??
   1.586 +MAKE-ALL (Poly/ML) ran perfectly.  It took 3:16 hours
   1.587 +
   1.588 +30 April
   1.589 +
   1.590 +HOL: installation of finite set notation: {x1,...,xn} (by Tobias Nipkow)
   1.591 +
   1.592 +HOL/set.thy,set.ML,fun.ML,equalities.ML: addition of rules for "insert",
   1.593 +new derivations for "singleton"
   1.594 +
   1.595 +HOL/llist.thy,llist.ML: changed {x.False} to {}
   1.596 +
   1.597 +**** New tar file placed on /homes/lcp (584K) **** 
   1.598 +
   1.599 +4 May
   1.600 +
   1.601 +MAKE-ALL (NJ 0.93) ran out of space in LK.
   1.602 +MAKE-ALL (Poly/ML) ran perfectly.  It took 3:14 hours
   1.603 +
   1.604 +Pure/Makefile: inserted "chmod u+w $(BIN)/Pure;" in case $(ML_DBASE) is
   1.605 +write-protected
   1.606 +
   1.607 +5 May
   1.608 +
   1.609 +HOL/list/not_Cons_self: renamed from l_not_Cons_l
   1.610 +HOL/list/not_CONS_self: new
   1.611 +
   1.612 +HOL/llist.thy/Lconst: changed type and def to remove Leaf
   1.613 +HOL/llist.ML: changed Lconst theorems
   1.614 +
   1.615 +6 May
   1.616 +
   1.617 +MAKE-ALL (Poly/ML) ran perfectly.  It took 3:18 hours
   1.618 +
   1.619 +** Installation of new HOL from Tobias **
   1.620 +
   1.621 +HOL/ex/{finite,prop-log} made like the ZF versions
   1.622 +HOL/hol.thy: type classes plus, minus, times; overloaded operators + - *
   1.623 +HOL/set: set enumeration via "insert"
   1.624 +         additions to set_cs and set_ss
   1.625 +HOL/set,subset,equalities: various lemmas to do with {}, insert and -
   1.626 +HOL/llist: One of the proofs needs one fewer commands
   1.627 +HOL/arith: many proofs require type constraints due to overloading
   1.628 +
   1.629 +** end Installation **
   1.630 +
   1.631 +ZF/ex/misc: added new lemmas from Abrial's paper
   1.632 +
   1.633 +7 May 
   1.634 +
   1.635 +HOL/llist.ML/LList_corec_subset1: deleted a fast_tac call; the previous
   1.636 +simplification now proves the subgoal.
   1.637 +
   1.638 +**** New tar file placed on /homes/lcp (584K) **** 
   1.639 +
   1.640 +** Installation of new simplifier from Tobias **
   1.641 +
   1.642 +The "case_splits" parameter of SimpFun is moved from the signature to the
   1.643 +simpset.  SIMP_CASE_TAC and ASM_SIMP_CASE_TAC are removed.  The ordinary
   1.644 +simplification tactics perform case splits if present in the simpset.
   1.645 +
   1.646 +The simplifier finds out for itself what constant is affected.  Instead of
   1.647 +supplying the pair (expand_if,"if"), supply just the rule expand_if.
   1.648 +
   1.649 +This change affects all calls to SIMP_CASE_TAC and all applications of SimpFun.
   1.650 +
   1.651 +MAKE-ALL (Poly/ML) ran perfectly.  It took 3:18 hours
   1.652 +
   1.653 +Cube/ex: UNTIL1, UNTIL_THM: replaced by standard tactics DEPTH_SOLVE_1 and
   1.654 +DEPTH_SOLVE
   1.655 +
   1.656 +HOL: installation of NORM tag for simplication.  How was it forgotten??
   1.657 +
   1.658 +HOL/hol.thy: declaration of NORM
   1.659 +HOL/simpdata: NORM_def supplied to SimpFun
   1.660 +
   1.661 +10 May
   1.662 +
   1.663 +MAKE-ALL (Poly/ML) ran perfectly.  It took 3:33 hours??
   1.664 +
   1.665 +11 May
   1.666 +
   1.667 +HOL/prod/Prod_eq: renamed Pair_eq
   1.668 +HOL/ex/lex-prod: wf_lex_prod: simplified proof
   1.669 +
   1.670 +HOL/fun/inj_eq: new
   1.671 +
   1.672 +HOL/llist/sumPairE: deleted, thanks to new simplifier's case splits!
   1.673 +
   1.674 +12 May
   1.675 +
   1.676 +MAKE-ALL (NJ 0.93) ran out of space in HOL.
   1.677 +MAKE-ALL (Poly/ML) failed in HOL.
   1.678 +HOL/Subst/utermlemmas/utlemmas_ss: deleted Prod_eq from the congruence rules
   1.679 +
   1.680 +13 May
   1.681 +
   1.682 +Pure/logic/flexpair: moved to term, with "equals" etc.  Now pervasive
   1.683 +Pure/logic/mk_flexpair: now exported
   1.684 +Pure/logic/dest_flexpair: new
   1.685 +Pure/goals/print_exn: now prints the error message for TERM and TYPE
   1.686 +
   1.687 +Pure/Syntax/sextension: now =?= has type ['a::{}, 'a] => prop because
   1.688 +flexflex pairs can have any type at all.  Thus == must have the same type.
   1.689 +
   1.690 +Pure/thm/flexpair_def: now =?= and == are equated for all 'a::{}.
   1.691 +
   1.692 +Pure/tctical/equal_abs_elim,equal_abs_elim_list: new (for METAHYPS fix)
   1.693 +Pure/tctical/METAHYPS: now works if new proof state has flexflex pairs
   1.694 +
   1.695 +Pure/Syntax/earley0A,syntax,lexicon: Tokens are represented by strings now,
   1.696 +not by integers.  (Changed by Tobias)
   1.697 +
   1.698 +*** Installation of more printing functions ***
   1.699 +
   1.700 +Pure/sign/sg: changed from a type abbrev to a datatype
   1.701 +Pure/type/type_sig: changed from a type abbrev to a datatype
   1.702 +These changes needed for abstract type printing in NJ
   1.703 +
   1.704 +Pure/tctical/print_sg,print_theory: new
   1.705 +
   1.706 +Pure/drule: new file containing derived rules and printing functions.
   1.707 +Mostly from tctical.ML, but includes rewriting rules from tactic.ML.
   1.708 +
   1.709 +Pure/ROOT: loads drule before tctical; TacticalFun,TacticFun,GoalsFun now
   1.710 +depend on Drule and have sharing constraints.
   1.711 +
   1.712 +14 May
   1.713 +
   1.714 +Installing new print functions for New Jersey: incompatible with Poly/ML!
   1.715 +
   1.716 +Pure/NJ/install_pp_nj: new (requires datatypes as above)
   1.717 +Pure/POLY/install_pp_nj: a dummy version
   1.718 +
   1.719 +Pure/ROOT: calls install_pp_nj to install printing for NJ
   1.720 +
   1.721 +*/ROOT: added extra install_pp calls (sg, theory, cterm, typ, ctyp) for
   1.722 +Poly/ML [ZF,LCF,Modal do not need them since they inherit them from another
   1.723 +logic -- make_database is not used]
   1.724 +
   1.725 +17 May
   1.726 +
   1.727 +MAKE-ALL (NJ 0.93) ran perfectly.  It took 3:57 hours??
   1.728 +
   1.729 +Pure/Syntax/lexicon: Yet another leaner and faster version ... (from Tobias)
   1.730 +
   1.731 +18 May
   1.732 +
   1.733 +MAKE-ALL (Poly/ML) ran perfectly.  It took 3:36 hours
   1.734 +
   1.735 +19 May
   1.736 +
   1.737 +ZF/equalities/Union_singleton,Inter_singleton: now refer to {b} instead of
   1.738 +complex assumptions
   1.739 +
   1.740 +20 May
   1.741 +
   1.742 +HOL/list: Tobias added the [x1,...,xn] notation and the functions hd, tl,
   1.743 +null and list_case.
   1.744 +
   1.745 +1 June
   1.746 +
   1.747 +MAKE-ALL (Poly/ML) ran perfectly.  It took 3:39 hours
   1.748 +
   1.749 +**** New tar file 92.tar.z placed on /homes/lcp (376K) **** 
   1.750 +
   1.751 +MAKE-ALL (NJ 0.93) ran perfectly.  It took 1:49 hours on albatross.
   1.752 +
   1.753 +Pure/tactic/dres_inst_tac,forw_inst_tac: now call the new
   1.754 +make_elim_preserve to preserve Var indexes when creating the elimination
   1.755 +rule.
   1.756 +
   1.757 +ZF/ex/ramsey: modified calls to dres_inst_tac
   1.758 +
   1.759 +2 June
   1.760 +
   1.761 +Pure/Thy/read/read_thy,use_thy: the .thy.ML file is now written to the
   1.762 +current directory, since the pathname may lead to a non-writeable area.
   1.763 +
   1.764 +HOL/arith: renamed / and // to div and mod
   1.765 +ZF/arith: renamed #/ and #// to div and mod
   1.766 +
   1.767 +MAKE-ALL (Poly/ML) ran perfectly.  It took 1:48 hours on albatross.
   1.768 +
   1.769 +**** New tar file 92.tar.z placed on /homes/lcp (376K) **** 
   1.770 +
   1.771 +Pure/NJ/commit: new dummy function
   1.772 +FOLP/ex/ROOT: inserted commit call to avoid Poly/ML problems
   1.773 +
   1.774 +make-all: now builds FOLP also!
   1.775 +
   1.776 +3 June
   1.777 +
   1.778 +ZF/zf.thy,HOL/list.thy,HOL/set.thy: now constructions involving {_}, [_],
   1.779 +<_,_> are formatted as {(_)}, [(_)], 
   1.780 +
   1.781 +MAKE-ALL (Poly/ML) ran perfectly.  It took 4:37 hours on muscovy (with FOLP).
   1.782 +
   1.783 +ZF/Makefile: removed obsolete target for .rules.ML
   1.784 +
   1.785 +All object-logic Makefiles: EXAMPLES ARE NO LONGER SAVED.  This saves disc
   1.786 +and avoids problems (in New Jersey ML) of writing to the currently
   1.787 +executing image.
   1.788 +
   1.789 +4 June
   1.790 +
   1.791 +Pure/logic/rewritec: now uses nets for greater speed.  Functor LogicFun now
   1.792 +takes Net as argument.
   1.793 +
   1.794 +Pure/ROOT: now loads net before logic.
   1.795 +
   1.796 +MAKE-ALL (Poly/ML) failed in ZF and HOL.
   1.797 +
   1.798 +LK/lk.thy: changed constant "not" to "Not" (for consistency with FOL)
   1.799 +
   1.800 +7 June
   1.801 +
   1.802 +Pure/tactic/is_letdig: moved to library
   1.803 +Pure/Syntax/lexicon/is_qld: deleted, was same as is_letdig
   1.804 +
   1.805 +MAKE-ALL (Poly/ML) ran perfectly.  It took 2:07 hours on albatross.
   1.806 +MAKE-ALL (NJ 0.93) ran perfectly.  It took 4:41 hours on dunlin.
   1.807 +
   1.808 +HOL/set/UN1,INT1: new union/intersection operators.  Binders UN x.B(x),
   1.809 +INT x.B(x).
   1.810 +
   1.811 +HOL/univ,llist: now use UN x.B(x) instead of Union(range(B))
   1.812 +
   1.813 +HOL/subset: added lattice properties for INT, UN (both forms)
   1.814 +
   1.815 +8 June
   1.816 +
   1.817 +MAKE-ALL (NJ 0.93) ran perfectly.  It took 4:45 hours on dunlin.
   1.818 +
   1.819 +**** New tar file 92.tar.z placed on /homes/lcp (384K) **** 
   1.820 +
   1.821 +14 June
   1.822 +
   1.823 +HOL/list.thy/List_rec_def: changed pred_sexp (a variable!) to pred_Sexp.
   1.824 +Using def_wfrec hides such errors!!
   1.825 +
   1.826 +**** New tar file 92.tar.gz placed on /homes/lcp (384K) **** 
   1.827 +
   1.828 +** NEW VERSION FROM MUNICH WITH ==-REWRITING **
   1.829 +
   1.830 +** The following changes are Toby's **
   1.831 +
   1.832 +type.ML:
   1.833 +
   1.834 +Renamed mark_free to freeze_vars and thaw_tvars to thaw_vars.
   1.835 +Added both functions to the signature.
   1.836 +
   1.837 +sign.ML:
   1.838 +
   1.839 +Added val subsig: sg * sg -> bool to signature.
   1.840 +Added trueprop :: prop and mark_prop : prop => prop to pure_sg.
   1.841 +
   1.842 +Added
   1.843 +
   1.844 +val freeze_vars: term -> term
   1.845 +val thaw_vars: term -> term
   1.846 +val strip_all_imp: term * int -> term list * term * int
   1.847 +
   1.848 +Moved rewritec_bottom and rewritec_top to thm.ML.
   1.849 +Only bottom-up rewriting supported any longer.
   1.850 +
   1.851 +thm.ML:
   1.852 +
   1.853 +Added
   1.854 +
   1.855 +(* internal form of conditional ==-rewrite rules *)
   1.856 +type meta_simpset
   1.857 +val add_mss: meta_simpset * thm list -> meta_simpset
   1.858 +val empty_mss: meta_simpset
   1.859 +val mk_mss: thm list -> meta_simpset
   1.860 +
   1.861 +val mark_prop_def: thm
   1.862 +val truepropI: thm
   1.863 +val trueprop_def: thm
   1.864 +
   1.865 +(* bottom-up conditional ==-rewriting with local ==>-assumptions *)
   1.866 +val rewrite_cterm: meta_simpset -> (thm -> thm list)
   1.867 +                   -> (meta_simpset -> thm list -> Sign.cterm -> thm)
   1.868 +                   -> Sign.cterm -> thm
   1.869 +val trace_simp: bool ref
   1.870 +
   1.871 +Simplified concl_of: call to Logic.skip_flexpairs redundant.
   1.872 +
   1.873 +drule.ML:
   1.874 +
   1.875 +Added
   1.876 +
   1.877 +(* rewriting *)
   1.878 +val asm_rewrite_rule: (thm -> thm list) -> thm list -> thm -> thm
   1.879 +val rewrite_goal_rule: (thm -> thm list) -> thm list -> int -> thm -> thm
   1.880 +val rewrite_goals_rule: (thm -> thm list) -> thm list -> thm -> thm
   1.881 +
   1.882 +(* derived concepts *)
   1.883 +val forall_trueprop_eq: thm
   1.884 +val implies_trueprop_eq: thm
   1.885 +val mk_trueprop_eq: thm -> thm
   1.886 +val reflexive_eq: thm
   1.887 +val reflexive_thm: thm
   1.888 +val trueprop_implies_eq: thm
   1.889 +val thm_implies: thm -> thm -> thm
   1.890 +val thm_equals: thm -> thm -> thm
   1.891 +
   1.892 +(*Moved here from tactic.ML:*)
   1.893 +val asm_rl: thm
   1.894 +val cut_rl: thm
   1.895 +val revcut_rl: thm
   1.896 +
   1.897 +tactic.ML:
   1.898 +
   1.899 +Added
   1.900 +
   1.901 +val asm_rewrite_goal_tac: (thm -> thm list) -> thm list -> int -> tactic
   1.902 +val asm_rewrite_goals_tac: (thm -> thm list) -> thm list -> tactic
   1.903 +val asm_rewrite_tac: (thm -> thm list) -> thm list -> tactic
   1.904 +val fold_goal_tac: thm list -> int -> tactic
   1.905 +val rewrite_goal_tac: thm list -> int -> tactic
   1.906 +
   1.907 +Moved to drule.ML:
   1.908 +val asm_rl: thm
   1.909 +val cut_rl: thm
   1.910 +val revcut_rl: thm
   1.911 +
   1.912 +goals.ML:
   1.913 +
   1.914 +Changed prepare_proof to make sure that rewriting with empty list of
   1.915 +meta-thms is identity.
   1.916 +
   1.917 +** End of Toby's changes **
   1.918 +
   1.919 +16 June
   1.920 +
   1.921 +Pure/sign/typ_of,read_ctyp: new
   1.922 +Pure/logic/dest_flexpair: now exported
   1.923 +
   1.924 +Pure/drule/flexpair_intr,flexpair_elim: new; fixes a bug in
   1.925 +flexpair_abs_elim_list
   1.926 +
   1.927 +HOL/equalities/image_empty,image_insert: new
   1.928 +HOL/ex/finite/Fin_imageI: new
   1.929 +
   1.930 +Installed Martin Coen's CCL as new object-logic
   1.931 +
   1.932 +17 June
   1.933 +
   1.934 +** More changes from Munich (Markus Wenzel) **
   1.935 +
   1.936 +Pure/library: added the, is_some, is_none, separate and improved space_implode
   1.937 +Pure/sign: Sign.extend now calls Syntax.extend with list of constants
   1.938 +Pure/symtab: added is_null
   1.939 +Pure/Syntax/sextension: added empty_sext
   1.940 +Pure/Syntax/syntax: changed Syntax.extend for compatibility with future version
   1.941 +
   1.942 +HOL now exceeds poly's default heap size. Hence HOL/Makefile needs to
   1.943 +specify -h 8000.
   1.944 +
   1.945 +HOL/univ/ntrunc_subsetD, etc: deleted the useless j<k assumption
   1.946 +
   1.947 +18 June
   1.948 +
   1.949 +MAKE-ALL (Poly/ML) ran perfectly.  It took 4:59 hours on dunlin (with CCL).
   1.950 +
   1.951 +Pure/sign/read_def_cterm: now prints the offending terms, as well as the
   1.952 +types, when exception TYPE is raised.
   1.953 +
   1.954 +HOL/llist: some tidying
   1.955 +
   1.956 +23 June
   1.957 +
   1.958 +HOL/llist/Lconst_type: generalized from Lconst(M): LList({M})
   1.959 +
   1.960 +24 June
   1.961 +
   1.962 +MAKE-ALL (Poly/ML) ran perfectly.  It took 2:23 hours on albatross (with CCL)
   1.963 +
   1.964 +MAKE-ALL (NJ 0.93) failed in CCL due to use of "abstraction" as an
   1.965 +identifier in CCL.ML
   1.966 +
   1.967 +**** New tar file 92.tar.gz placed on /homes/lcp (384K) **** (with CCL)
   1.968 +
   1.969 +CCL/ROOT: added ".ML" extension to use commands for NJ compatibility
   1.970 +
   1.971 +25 June
   1.972 +
   1.973 +MAKE-ALL (Poly/ML) ran perfectly.  It took 2:23 hours on albatross.
   1.974 +MAKE-ALL (NJ 0.93) failed in HOL due to lack of ".ML" extension
   1.975 +
   1.976 +HOL/fun/rangeE,imageE: eta-expanded f to get variable name preservation
   1.977 +
   1.978 +HOL/llist/iterates_equality,lmap_lappend_distrib: tidied
   1.979 +
   1.980 +28 June
   1.981 +
   1.982 +HOL/set/UN1_I: made the Var and Bound variables agree ("x") to get variable
   1.983 +name preservation 
   1.984 +
   1.985 +HOL/llist: co-induction rules applied with res_inst_tac to state the
   1.986 +bisimulation directly
   1.987 +
   1.988 +2 July
   1.989 +
   1.990 +MAKE-ALL (NJ 0.93) ran perfectly.  It took 2:10 hours on albatross.
   1.991 +MAKE-ALL (Poly/ML) ran perfectly.  It took 2:23 hours on albatross.
   1.992 +
   1.993 +92/Makefile/$(BIN)/Pure: changed echo makefile= to echo database=
   1.994 +
   1.995 +**** New tar file 92.tar.gz placed on /homes/lcp (424K) **** (with CCL)
   1.996 +
   1.997 +
   1.998 +** NEW VERSION FROM MUNICH WITH ABSTRACT SYNTAX TREES & NEW PARSER **
   1.999 +
  1.1000 +I have merged in the changes shown above since 24 June
  1.1001 +
  1.1002 +CHANGES LOG OF Markus Wenzel (MMW)
  1.1003 +=======
  1.1004 +
  1.1005 +29-Jun-1993 MMW
  1.1006 +  *** Beta release of new syntax module ***
  1.1007 +  (should be 99% backwards compatible)
  1.1008 +
  1.1009 +  Pure/Thy/ROOT.ML
  1.1010 +    added keywords for "translations" section
  1.1011 +
  1.1012 +  Pure/Thy/syntax.ML
  1.1013 +    minor cleanup
  1.1014 +    added syntax for "translations" section
  1.1015 +    .*.thy.ML files now human readable
  1.1016 +    .*.thy.ML used to be generated incorrectly if no mixfix but "ML" section
  1.1017 +    "ML" section no longer demands any definitions (parse_translation, ...)
  1.1018 +
  1.1019 +  Pure/Thy/read.ML
  1.1020 +    read_thy: added close_in
  1.1021 +    added file_exists (not perfect)
  1.1022 +    use_thy: now uses file_exists
  1.1023 +
  1.1024 +  Pure/thm.ML
  1.1025 +    added syn_of: theory -> syntax
  1.1026 +
  1.1027 +  Pure/Makefile
  1.1028 +    SYNTAX_FILES: added Syntax/ast.ML
  1.1029 +
  1.1030 +  Pure/Syntax/pretty.ML
  1.1031 +    added str_of: T -> string
  1.1032 +
  1.1033 +  Pure/Syntax/ast.ML
  1.1034 +    added this file
  1.1035 +
  1.1036 +  Pure/Syntax/extension.ML
  1.1037 +  Pure/Syntax/parse_tree.ML
  1.1038 +  Pure/Syntax/printer.ML
  1.1039 +  Pure/Syntax/ROOT.ML
  1.1040 +  Pure/Syntax/sextension.ML
  1.1041 +  Pure/Syntax/syntax.ML
  1.1042 +  Pure/Syntax/type_ext.ML
  1.1043 +  Pure/Syntax/xgram.ML
  1.1044 +    These files have been completely rewritten, though the global structure
  1.1045 +    is similar to the old one.
  1.1046 +
  1.1047 +
  1.1048 +30-Jun-1993 MMW
  1.1049 +  New versions of HOL and Cube: use translation rules wherever possible;
  1.1050 +
  1.1051 +  HOL/hol.thy
  1.1052 +    cleaned up
  1.1053 +    removed alt_tr', mk_bindopt_tr'
  1.1054 +    alternative binders now implemented via translation rules and mk_alt_ast_tr'
  1.1055 +
  1.1056 +  HOL/set.thy
  1.1057 +    cleaned up
  1.1058 +    removed type "finset"
  1.1059 +    now uses category "args" for finite sets
  1.1060 +    junked "ML" section
  1.1061 +    added "translations" section
  1.1062 +
  1.1063 +  HOL/list.thy
  1.1064 +    cleaned up
  1.1065 +    removed type "listenum"
  1.1066 +    now uses category "args" for lists
  1.1067 +    junked "ML" section
  1.1068 +    added "translations" section
  1.1069 +
  1.1070 +  Cube/cube.thy
  1.1071 +    cleaned up
  1.1072 +    changed indentation of Lam and Pi from 2 to 3
  1.1073 +    removed qnt_tr, qnt_tr', no_asms_tr, no_asms_tr'
  1.1074 +    fixed fun_tr': all but one newly introduced frees will have type dummyT
  1.1075 +    added "translations" section
  1.1076 +
  1.1077 +
  1.1078 +30-Jun-1993, 05-Jul-1993 MMW
  1.1079 +  Improved toplevel pretty printers:
  1.1080 +    - unified interface for POLY and NJ;
  1.1081 +    - print functions now insert atomic string into the toplevel's pp stream,
  1.1082 +      rather than writing it to std_out (advantage: output appears at the
  1.1083 +      correct position, disadvantage: output cannot be broken);
  1.1084 +  (Is there anybody in this universe who exactly knows how Poly's install_pp
  1.1085 +  is supposed to work?);
  1.1086 +
  1.1087 +  Pure/NJ.ML
  1.1088 +    removed dummy install_pp
  1.1089 +    added make_pp, install_pp
  1.1090 +
  1.1091 +  Pure/POLY.ML
  1.1092 +    removed dummy install_pp_nj
  1.1093 +    added make_pp
  1.1094 +
  1.1095 +  Pure/ROOT.ML
  1.1096 +    removed install_pp_nj stuff
  1.1097 +
  1.1098 +  Pure/drule.ML
  1.1099 +    added str_of_sg, str_of_theory, str_of_thm
  1.1100 +
  1.1101 +  Pure/install_pp.ML
  1.1102 +    added this file
  1.1103 +
  1.1104 +  Pure/sign.ML
  1.1105 +    added str_of_term, str_of_typ, str_of_cterm, str_of_ctyp
  1.1106 +
  1.1107 +  Pure/goals.ML
  1.1108 +    added str_of_term, str_of_typ
  1.1109 +
  1.1110 +  CTT/ROOT.ML
  1.1111 +  Cube/ROOT.ML
  1.1112 +  FOL/ROOT.ML
  1.1113 +  FOLP/ROOT.ML
  1.1114 +  HOL/ROOT.ML
  1.1115 +  LK/ROOT.ML
  1.1116 +    replaced install_pp stuff by 'use "../Pure/install_pp.ML"'
  1.1117 +
  1.1118 +
  1.1119 +01-Jul-1993 MMW
  1.1120 +  Misc small fixes
  1.1121 +
  1.1122 +  CCL/ROOT.ML
  1.1123 +  HOL/ROOT.ML
  1.1124 +    added ".ML" suffix to some filenames
  1.1125 +
  1.1126 +  HOL/ex/unsolved.ML
  1.1127 +    replaced HOL_Rule.thy by HOL.thy
  1.1128 +
  1.1129 +  Pure/NJ.ML
  1.1130 +    quit was incorrectly int -> unit
  1.1131 +
  1.1132 +END MMW CHANGES
  1.1133 +
  1.1134 +Pure/Syntax/sextension/eta_contract: now initially false 
  1.1135 +
  1.1136 +Pure/library/cat_lines: no longer calls "distinct"
  1.1137 +Pure/sign: replaced to calls of implode (map (apr(op^,"\n") o ... by cat_lines
  1.1138 +NB This could cause duplicate error messages from Pure/sign and Pure/type
  1.1139 +
  1.1140 +Pure/goals/prove_goalw: now prints some of the information from print_exn
  1.1141 +
  1.1142 +9 July
  1.1143 +
  1.1144 +MAKE-ALL (Poly/ML) ran perfectly.  It took 2:26 hours on albatross.
  1.1145 +
  1.1146 +**** New tar file 93.tar.gz placed on /homes/lcp (480K) **** 
  1.1147 +
  1.1148 +12 July
  1.1149 +
  1.1150 +MAKE-ALL (NJ 0.93) ran perfectly.  It took 2:13 hours on albatross.
  1.1151 +MAKE-ALL (Poly/ML) ran perfectly.  It took 2:25 hours on albatross.
  1.1152 +
  1.1153 +22 July
  1.1154 +
  1.1155 +ZF/zf.thy: new version from Marcus Wenzel
  1.1156 +
  1.1157 +ZF: ** installation of inductive definitions **
  1.1158 +
  1.1159 +changing the argument order of "split"; affects fst/snd too
  1.1160 +sum.thy zf.thy ex/bin.thy ex/integ.thy ex/simult.thy ex/term.thy
  1.1161 +pair.ML  ex/integ.ML
  1.1162 +
  1.1163 +changing the argument order of "case" and adding "Part": sum.thy sum.ML
  1.1164 +
  1.1165 +ZF/zf.ML/rev_subsetD,rev_bspec: new
  1.1166 +
  1.1167 +ZF/mono: new rules for implication
  1.1168 +ZF/mono/Collect_mono: now for use with implication rules
  1.1169 +
  1.1170 +ZF/zf.ML/ballE': renamed rev_ballE
  1.1171 +
  1.1172 +ZF/list.thy,list.ML: files renamed list-fn.thy, list-fn.ML
  1.1173 +ZF/list.ML: new version simply holds the datatype definition
  1.1174 +NB THE LIST CONSTRUCTORS ARE NOW Nil/Cons, not 0/Pair.
  1.1175 +
  1.1176 +ZF/extend_ind.ML, datatype.ML: new files
  1.1177 +ZF/fin.ML: moved from ex/finite.ML
  1.1178 +
  1.1179 +23 July
  1.1180 +
  1.1181 +ZF/ex/sexp: deleted this example -- it seems hardly worth the trouble of
  1.1182 +porting.
  1.1183 +
  1.1184 +ZF/ex/bt.thy,bt.ML: files renamed bt-fn.thy, bt-fn.ML
  1.1185 +ZF/ex/bt.ML: new version simply holds the datatype definition
  1.1186 +
  1.1187 +ZF/ex/term.thy,term.ML: files renamed term-fn.thy, term-fn.ML
  1.1188 +ZF/ex/term.ML: new version simply holds the datatype definition
  1.1189 +
  1.1190 +ZF/sum/InlI,InrI: renamed from sum_InlI, sum_InlI
  1.1191 +
  1.1192 +26 July
  1.1193 +
  1.1194 +ZF/univ/rank_ss: new, for proving recursion equations
  1.1195 +
  1.1196 +ZF/domrange/image_iff,image_singleton_iff,vimage_iff,vimage_singleton_iff,
  1.1197 +field_of_prod:new
  1.1198 +
  1.1199 +ZF/domrange/field_subset: modified
  1.1200 +
  1.1201 +ZF/list/list_cases: no longer proved by induction!
  1.1202 +ZF/wf/wf_trancl: simplified proof
  1.1203 +
  1.1204 +ZF/equalities: new laws for field
  1.1205 +
  1.1206 +29 July
  1.1207 +
  1.1208 +ZF/trancl/trancl_induct: new
  1.1209 +ZF/trancl/rtrancl_induct,trancl_induct: now with more type information
  1.1210 +
  1.1211 +** More changes from Munich (Markus Wenzel) **
  1.1212 +
  1.1213 +Update of new syntax module (aka macro system): mostly internal cleanup and
  1.1214 +polishing;
  1.1215 +
  1.1216 +  Pure/Syntax/*
  1.1217 +    added Ast.stat_norm
  1.1218 +    added Syntax.print_gram, Syntax.print_trans, Syntax.print_syntax
  1.1219 +    cleaned type and Pure syntax: "_CLASSES" -> "classes", "_SORTS" -> "sorts",
  1.1220 +     "_==>" -> "==>", "_fun" -> "fun", added some space for printing
  1.1221 +    Printer: partial fix of the "PROP <aprop>" problem: print "PROP " before
  1.1222 +      any Var or Free of type propT
  1.1223 +    Syntax: added ndependent_tr, dependent_tr'
  1.1224 +
  1.1225 +  Pure/sign.ML: removed declaration of "==>" (now in Syntax.pure_sext)
  1.1226 +
  1.1227 +Changes to object logics: minor cleanups and replacement of most remaining ML
  1.1228 +translations by rewrite rules (see also file "Translations");
  1.1229 +
  1.1230 +  ZF/zf.thy
  1.1231 +    added "translations" section
  1.1232 +    removed all parse/print translations except ndependent_tr, dependent_tr'
  1.1233 +    fixed dependent_tr': all but one newly introduced frees have type dummyT
  1.1234 +    replaced id by idt in order to make terms rereadable if !show_types
  1.1235 +
  1.1236 +  Cube/cube.thy
  1.1237 +    removed necontext
  1.1238 +    replaced fun_tr/tr' by ndependent_tr/dependent_tr'
  1.1239 +
  1.1240 +  CTT/ctt.thy
  1.1241 +    added translations rules for PROD and SUM
  1.1242 +    removed dependent_tr
  1.1243 +    removed definitions of ndependent_tr, dependent_tr'
  1.1244 +
  1.1245 +  HOL/set.thy: replaced id by idt
  1.1246 +
  1.1247 +  CCL/ROOT.ML: Logtic -> Logic
  1.1248 +
  1.1249 +  CCL/set.thy
  1.1250 +    added "translations" section
  1.1251 +    removed "ML" section
  1.1252 +    replaced id by idt
  1.1253 +
  1.1254 +  CCL/types.thy
  1.1255 +    added "translations" section
  1.1256 +    removed definitions of ndependent_tr, dependent_tr'
  1.1257 +    replaced id by idt
  1.1258 +
  1.1259 +Yet another improvement of toplevel pretty printers: output now breakable;
  1.1260 +
  1.1261 +  Pure/NJ.ML Pure/POLY.ML improved make_pp
  1.1262 +
  1.1263 +  Pure/install_pp.ML: replaced str_of_* by pprint_*
  1.1264 +
  1.1265 +  Pure/drule.ML: replaced str_of_{sg,theory,thm} by pprint_*
  1.1266 +
  1.1267 +  Pure/sign.ML: replaced str_of_{term,typ,cterm,ctyp} by pprint_*
  1.1268 +
  1.1269 +  Pure/goals.ML: fixed and replaced str_of_{term,typ} by pprint_*
  1.1270 +
  1.1271 +  Pure/Syntax/pretty.ML: added pprint, quote
  1.1272 +
  1.1273 +Minor changes and additions;
  1.1274 +
  1.1275 +  Pure/sign.ML: renamed stamp "PURE" to "Pure"
  1.1276 +
  1.1277 +  Pure/library.ML
  1.1278 +    added quote: string -> string
  1.1279 +    added to_lower: string -> bool
  1.1280 +
  1.1281 +  Pure/NJ.ML,POLY.ML: added file_info of Carsten Clasohm
  1.1282 +
  1.1283 +30 July
  1.1284 +
  1.1285 +MAKE-ALL (Poly/ML) ran perfectly.
  1.1286 +
  1.1287 +Pure/goals/print_sign_exn: new, takes most code from print_exn
  1.1288 +Pure/goals/prove_goalw: displays exceptions using print_sign_exn
  1.1289 +
  1.1290 +Pure/drule/print_sg: now calls pretty_sg to agree with pprint_sg
  1.1291 +
  1.1292 +Pure/library,...: replaced front/nth_tail by take/drop.
  1.1293 +
  1.1294 +Pure/term/typ_tfrees,typ_tvars,term_tfrees,term_tvars: new
  1.1295 +thm/mk_rew_triple, drule/types_sorts, sign/zero_tvar_indices: now use the above
  1.1296 +
  1.1297 +Pure/logic/add_term_vars,add_term_frees,insert_aterm,atless:
  1.1298 +moved to term, joining similar functions for type variables;
  1.1299 +Logic.vars and Logic.frees are now term_vars and term_frees
  1.1300 +
  1.1301 +Pure/term/subst_free: new
  1.1302 +
  1.1303 +Pure/tactic/is_fact: newly exported
  1.1304 +
  1.1305 +Provers/simp/mk_congs: uses filter_out is_fact to delete trivial cong rules
  1.1306 +
  1.1307 +Pure/tactic/rename_last_tac: now uses Syntax.is_identifier instead of
  1.1308 +forall is_letdig
  1.1309 +
  1.1310 +**** New tar file 93.tar.gz placed on /homes/lcp (448K) **** 
  1.1311 +
  1.1312 +2 August
  1.1313 +
  1.1314 +MAKE-ALL (NJ 0.93) failed in ZF due to Compiler bug: elabDecl:open:FctBodyStr
  1.1315 +MAKE-ALL (Poly/ML) failed in ZF/enum.  It took 2:33 hours on albatross.
  1.1316 +
  1.1317 +Pure/drule/triv_forall_equality: new
  1.1318 +Pure/tactic/prune_params_tac: new
  1.1319 +
  1.1320 +Provers/hypsubst/bound_hyp_subst_tac: new, safer than hyp_subst_tac
  1.1321 +
  1.1322 +3 August
  1.1323 +
  1.1324 +Pure/tactic/rule_by_tactic: new
  1.1325 +
  1.1326 +ZF/perm/compEpair: now proved via rule_by_tactic
  1.1327 +
  1.1328 +ZF/extend_ind/cases,mk_cases: new
  1.1329 +ZF/datatype/mk_free: new
  1.1330 +ZF/list: now calls List.mk_cases
  1.1331 +
  1.1332 +4 August
  1.1333 +
  1.1334 +Provers/slow_tac,slow_best_tac: new
  1.1335 +
  1.1336 +5 August
  1.1337 +
  1.1338 +MAKE-ALL (Poly/ML) failed in ZF
  1.1339 +
  1.1340 +ZF/sum/sumE2: deleted since unused
  1.1341 +ZF/sum/sum_iff,sum_subset_iff,sum_equal_iff: new
  1.1342 +ZF/univ/Transset_Vfrom: new; used in proof of Transset_Vset
  1.1343 +
  1.1344 +6 August
  1.1345 +
  1.1346 +Pure/goals/prepare_proof: after "Additional hypotheses", now actually
  1.1347 +prints them!
  1.1348 +
  1.1349 +ZF/ordinal/Transset_Union_family, Transset_Inter_family: renamed from
  1.1350 +Transset_Union, Transset_Inter
  1.1351 +
  1.1352 +ZF/ordinal/Transset_Union: new 
  1.1353 +ZF/univ/pair_in_univ: renamed Pair_in_univ
  1.1354 +
  1.1355 +ZF/mono/product_mono: generalized to Sigma_mono; changed uses in trancl, univ
  1.1356 +
  1.1357 +ZF/lfp/lfp_Tarski,def_lfp_Tarski: renamed from Tarski,def_Tarski; changed
  1.1358 +uses in extend_ind.ML, nat.ML, trancl.ML.
  1.1359 +
  1.1360 +ZF/ex/misc: Schroeder-Bernstein Theorem moved here from lfp.ML
  1.1361 +
  1.1362 +ZF/fixedpt.thy,.ML: renamed from lfp.thy,.ML, and gfp added
  1.1363 +
  1.1364 +9 August
  1.1365 +
  1.1366 +ZF/zf.thy/ndependent_tr,dependent_tr': deleted, since they are now on
  1.1367 +Syntax/sextension. 
  1.1368 +
  1.1369 +11 August
  1.1370 +
  1.1371 +Pure/library.ML: added functions
  1.1372 +assocs: (''a * 'b list) list -> ''a -> 'b list
  1.1373 +transitive_closure: (''a * ''a list) list -> (''a * ''a list) list
  1.1374 +
  1.1375 +Pure/type.ML: deleted (inefficient) transitive_closure