summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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