1 EDITS TO THE ISABELLE SYSTEM FOR 1993
5 */README: Eliminated references to Makefile.NJ, which no longer exists.
7 **** New tar file placed on /homes/lcp (464K) ****
11 Provers/simp/pr_goal_lhs: now distinct from pr_goal_concl so that tracing
12 prints conditions correctly.
14 {CTT/arith,HOL/ex/arith/ZF/arith}/add_mult_distrib: renamed from
15 add_mult_dist, to agree with the other _distrib rules
19 Pure/Syntax/type_ext.ML: "I have fixed a few anomalies in the pretty
20 printing annotations for types. Only the layout has changed." -- Toby
24 {CTT/arith,HOL/ex/arith/ZF/arith}/add_inverse_diff: renamed to add_diff_inverse
28 ZF/ex/equiv: new theory of equivalence classes
29 ZF/ex/integ: new theory of integers
30 HOL/set.thy: added indentation of 3 to all binding operators
32 ZF/bool/boolI0,boolI1: renamed as bool_0I, bool_1I
36 MAKE-ALL (NJ 0.75) ran perfectly. It took 3:19 hours!?
38 ZF/bool/not,and,or,xor: new
42 ZF/ex/bin: new theory of binary integer arithmetic
46 MAKE-ALL (Poly/ML) ran perfectly. It took 6:33 hours???
47 (ZF took almost 5 hours!)
49 **** New tar file placed on /homes/lcp (472K) ****
51 HOL/set/UN_cong,INT_cong: new
52 HOL/subset/mem_rews,set_congs,set_ss: new
53 HOL/simpdata/o_apply: new; added to HOL_ss
57 Pure/Thy/syntax/mk_structure: the dummy theory created by type infixes is
58 now called name^"(type infix)" instead of "", avoid triggering a spurious
59 error "Attempt to merge different versions of theory: " in
60 Pure/sign/merge_stamps
64 MAKE-ALL (Poly/ML) ran perfectly. It took 2:48 hours. Runs in 1992 took
65 under 2:20 hours, but the new files in ZF/ex take time: nearly 23 minutes
66 according to make10836.log.
68 Pure/Thy/scan/comment: renamed from komt
69 Pure/Thy/scan/numeric: renamed from zahl
71 Pure/Syntax/syntax,lexicon,type_ext,extension,sextension: modified by
72 Tobias to change ID, TVAR, ... to lower case.
74 Cube/cube.thy,HOL/hol.thy,HOL/set.thy,CTT/ctt.thy,LK/lk.thy,ZF/zf.thy: now
75 with ID, ... in lower case and other tidying
79 MAKE-ALL (Poly/ML) ran perfectly. It took 2:50 hours.
83 HOL/nat/nat_ss: now includes the rule Suc_less_eq: (Suc(m) < Suc(n)) = (m<n)
84 and the nat_case rules and congruence rules
86 HOL/sum/sumE: now has the "strong" form with equality assumptions. WAS
87 val prems = goalw Sum.thy [Inl_def,Inr_def]
88 "[| !!x::'a. P(Inl(x)); !!y::'b. P(Inr(y)) \
90 by (res_inst_tac [("t","s")] (Rep_Sum_inverse RS subst) 1);
91 by (rtac (rewrite_rule [Sum_def] Rep_Sum RS CollectE) 1);
92 by (REPEAT (eresolve_tac [disjE,exE,ssubst] 1 ORELSE resolve_tac prems 1));
98 Pure/Thy/parse: now list_of admits the empty phrase, while listof_1 does not
99 Pure/Thy/syntax: uses new list_of, list_of1
103 HOL/ex/arith: moved to main HOL directory
104 HOL/prod: now define the type "unit" and constant "(): unit"
108 HOL/arith: eliminated redefinitions of nat_ss and arith_ss
112 MAKE-ALL (Poly/ML) ran perfectly. It took 2:50 hours.
114 Pure/Thy/scan/string: now correctly recognizes ML-style strings.
118 MAKE-ALL (NJ 0.75) ran perfectly. It took 1:37 hours (on albatross)
119 MAKE-ALL (NJ 0.75) ran perfectly. It took 2:42 hours (on dunlin)
120 MAKE-ALL (Poly/ML) ran perfectly. It took 2:53 hours (on dunlin)
122 **** New tar file placed on /homes/lcp (480K) ****
126 Pure/Syntax/earley0A/compile_xgram: Tobias deleted the third argument, as
129 Pure/Syntax/earley0A: modified accordingly.
133 MAKE-ALL (NJ 0.75) ran perfectly. It took 3:37 hours
134 MAKE-ALL (Poly/ML) ran perfectly. It took 2:52 hours
136 **** New tar file placed on /homes/lcp (480K) ****
140 MAKE-ALL (NJ 0.93) ran perfectly. It took 3:30 hours
144 HOL/fun/image_eqI: fixed bad pattern
148 MAKE-ALL (Poly/ML) failed in HOL!
150 HOL/fun: moved "mono" proofs to HOL/subset, since they rely on subset laws
155 ZF/ex/misc: new example from Bledsoe
159 ZF/perm: two new theorems inspired by Pastre
163 Weakened congruence rules for HOL: speeds simplification considerably by
164 NOT simplifying the body of a conditional or eliminator.
166 HOL/simpdata/mk_weak_congs: new, to make weakened congruence rules
168 HOL/simpdata/congs: renamed HOL_congs and weakened the "if" rule
170 HOL/simpdata/HOL_congs: now contains polymorphic rules for the overloaded
173 HOL/prod: weakened the congruence rule for split
174 HOL/sum: weakened the congruence rule for case
175 HOL/nat: weakened the congruence rule for nat_case and nat_rec
176 HOL/list: weakened the congruence rule for List_rec and list_rec
178 HOL & test rebuilt perfectly
180 Pure/goals/prepare_proof/mkresult: fixed bug in signature check. Now
181 compares the FINAL signature with that from the original theory.
183 Pure/goals/prepare_proof: ensures that [prove_]goalw checks that the
184 definitions do not update the proof state.
188 MAKE-ALL (Poly/ML) ran perfectly.
192 MAKE-ALL (Poly/ML) failed in HOL/ex/Substitutions
194 HOL/ex/Subst/setplus: changed Set.thy to Setplus.thy where
197 ZF/perm: proved some rules about inj and surj
199 ZF/ex/misc: did some of Pastre's examples
201 Pure/library/gen_ins,gen_union: new
203 HOL/ex/Subst/subst: renamed rangeE to srangeE
207 MAKE-ALL (Poly/ML) failed in HOL/ex/term due to renaming of list_ss in
210 HOL/list/list_congs: new; re-organized simpsets a bit
212 Pure/goals/sign_error: new
214 Pure/goals/prepare_proof,by_com: now print the list of new theories when
215 the signature of the proof state changes
217 HOL/prod,sexp: renamed fst, snd to fst_conv, snd_conv to avoid over-writing
218 the library functions fst, snd
220 HOL/fun/image_compose: new
224 MAKE-ALL (NJ 0.93) ran perfectly. It took 3:50 hours
225 MAKE-ALL (Poly/ML) ran perfectly. It took 3:21 hours
226 Much slower now (about 30 minutes!) because of HOL/ex/Subst
228 **** New tar file placed on /homes/lcp (504K) ****
230 ZF/pair,simpdata: renamed fst, snd to fst_conv, snd_conv to avoid over-writing
231 the library functions fst, snd
233 HOL/prod/prod_fun_imageI,E: new
235 HOL/ex/Subst/Unify: renamed to Unifier to avoid clobbering structure Unify
240 HOL/trancl/comp_subset_Sigma: new
243 HOL/Subst: moved from HOL/ex/Subst to shorten pathnames
244 HOL/Makefile: target 'test' now loads Subst/ROOT separately
246 *** Installation of gfp, coinduction, ... to HOL ***
249 HOL/univ,sexp,list: replaced with new version
251 Sexp is now the set of all well-founded trees, each of type 'a node set.
252 There is no longer a type 'sexp'. Initial algebras require more explicit
253 type checking than before. Defining a type 'sexp' would eliminate this,
254 but would also require a whole new set of primitives, similar to those
255 defined in univ.thy but restricted to well-founded trees.
259 Pure/thm: renamed 'bires' to 'eres' in many places (not exported) --
260 biresolution now refers to resolution with (flag,rule) pairs.
262 Pure/thm/bicompose_aux: SOUNDNESS BUG concerning variable renaming. A Var in
263 a premise was getting renamed when its occurrence in the flexflex pairs was
264 not. Martin Coen supplied the following proof of True=False in HOL:
266 val [prem] = goal Set.thy "EX a:{c}.p=a ==> p=c";
267 br (prem RS bexE) 1; be ssubst 1; be singletonD 1;
270 val rls = [refl] RL [bexI] RL [l1];
272 goal Set.thy "True = False";
273 brs rls 1; br singletonI 1;
276 Marcus Moore noted that the error only occurred with
277 Logic.auto_rename:=false. Elements of the fix:
279 1. rename_bvs, rename_bvars and bicompose_aux/newAs take tpairs (the
280 existing flex-flex pairs) as an extra argument. rename_bvs preserves all
283 2. bicompose_aux/tryasms and res now unpack the "cell" and supply its tpairs
286 HOL/lfp,gfp,ex/set: renamed Tarski to lfp_Tarski
288 HOL/lfp,list,llist,nat,sexp,trancl,Subst/uterm,ex/simult,ex/term: renamed
289 def_Tarski to def_lfp_Tarski
293 MAKE-ALL (NJ 0.93) ran perfectly. It took 4:25 hours!
294 MAKE-ALL (Poly/ML) ran perfectly. It took 3:54 hours! (jobs overlapped)
296 Pure/Thy/scan/is_digit,is_letter: deleted. They are already in
297 Pure/library, and these versions used non-Standard string comparisons!
299 Repairing a fault reported by David Aspinall:
300 show_types := true; read "a"; (* followed by 'prin it' for NJ *)
301 Raises exception LIST "hd". Also has the side effect of leaving
302 show_types set at false.
304 Pure/goals/read: no longer creates a null TVar
305 Pure/Syntax/lexicon/string_of_vname: now handles null names
306 Pure/Syntax/printer/string_of_typ: tidied
308 /usr/groups/theory/isabelle/92/Pure/thm: replaced by new version to fix bug
309 MAKE-ALL on this directory ran perfectly
310 /usr/groups/theory/ml-aftp/Isabelle92.tar.Z: replaced by new version
314 MAKE-ALL (NJ 0.93) ran perfectly. It took 4:14 hours!
315 MAKE-ALL (Poly/ML) ran perfectly. It took 3:43 hours!
317 **** New tar file placed on /homes/lcp (518K) ****
321 ZF/univ/cons_in_Vfrom: deleted "[| a: Vfrom(A,i); b<=Vfrom(A,i) |] ==>
322 cons(a,b) : Vfrom(A,succ(i))" since it was useless.
326 MAKE-ALL (Poly/ML) ran perfectly. It took 3:49 hours!
328 **** New tar file placed on /homes/lcp (520K) ****
330 **** Updates for pattern unification (Tobias Nipkow) ****
332 Pure/pattern.ML: new, pattern unification
334 Pure/Makefile and ROOT.ML: included pattern.ML
336 Pure/library.ML: added predicate downto0
338 Pure/unify.ML: call pattern unification first. Removed call to could_unify.
340 FOL/Makefile/FILES: now mentions ifol.ML (previously repeated fol.ML instead)
342 **** Installation of Martin Coen's FOLP (FOL + proof objects) ****
344 renamed PFOL, PIFOL to FOLP, IFOLP, etc.
348 MAKE-ALL (NJ 0.93) ran perfectly. It took 4:05 hours!
349 MAKE-ALL (Poly/ML) ran perfectly. It took 3:31 hours!
351 **** New tar file placed on /homes/lcp (576K) ****
353 **** Installation of Discrimination Nets ****
355 *Affected files (those mentioning Stringtree, compat_thms or rtr_resolve_tac)
356 Pure/ROOT.ML,goals.ML,stringtree.ML,tactic.ML
360 *Affected files (those mentioning compat_resolve_tac)
365 Pure/stringtree: saved on Isabelle/old
367 Pure/Makefile/FILES: now mentions net.ML, not stringtree.ML
368 Pure/ROOT: now mentions net.ML, not stringtree.ML
370 Pure/goals/compat_goal: DELETED
372 Pure/tactic/compat_thms,rtr_resolve_tac,compat_resolve_tac,insert_thm,
373 delete_thm,head_string: DELETED
375 Pure/tactic/biresolve_from_nets_tac, bimatch_from_nets_tac,
376 net_biresolve_tac, net_bimatch_tac, resolve_from_net_tac, match_from_net_tac,
377 net_resolve_tac, net_match_tac: NEW
379 Pure/tactic/filt_resolve_tac: new implementation using nets!
381 Provers/simp: replaced by new version
383 Provers/typedsimp: changed compat_resolve_tac to filt_resolve_tac and
386 CTT/ctt.ML: changed compat_resolve_tac to filt_resolve_tac
387 ZF/simpdata/typechk_step_tac: changed compat_resolve_tac to filt_resolve_tac
391 HOL/ex/meson/ins_term,has_reps: replaced Stringtree by Net
395 Provers/simp/cong_const: new, replaces head_string call in cong_consts
396 Provers/simp: renamed variables: atomic to at and cong_consts to ccs
398 ZF/ex/bin/integ_of_bin_type: proof required reordering of rules --
399 typechk_tac now respects this ordering!
405 Logics/CTT: Removed mention of compat_resolve_tac
406 Ref/goals: deleted compat_goal's entry
408 Provers/hypsubst/lasthyp_subst_tac: deleted
410 FOLP/ROOT/dest_eq: corrected; now hyp_subst_tac works!
414 MAKE-ALL (NJ 0.93) ran perfectly. It took 4:03 hours!
415 MAKE-ALL (Poly/ML) ran perfectly. It took 3:28 hours!
417 FOLP/{int-prover,classical}/safe_step_tac: uses eq_assume_tac, not assume_tac
418 FOLP/{int-prover,classical}/inst_step_tac: restored, calls assume and mp_tac
419 FOLP/{int-prover,classical}/step_tac: calls inst_step_tac
421 {FOL,FOLP}/int-prover/safe_brls: removed (asm_rl,true) since assume_tac is
424 FOLP/ifolp/uniq_assume_tac: new, since eq_assume_tac is almost useless
426 FOLP/{int-prover,classical}/uniq_mp_tac: replace eq_mp_tac and call
429 Provers/classical: REPLACED BY 'NET' VERSION!
433 MAKE-ALL (Poly/ML) failed in ZF and ran out of quota for Cube.
435 Unification bug (nothing to do with pattern unification)
436 Cleaning of flex-flex pairs attempts to remove all occurrences of bound
437 variables not common to both sides. Arguments containing "banned" bound
438 variables are deleted -- but this should ONLY be done if the occurrence is
441 unify/CHANGE_FAIL: new, for flexible occurrence of bound variable
442 unify/change_bnos: now takes "flex" as argument, indicating path status
446 MAKE-ALL (Poly/ML) failed in HOL (ASM_SIMP_TAC redefined!) and LK
448 LK/ex/hard-quant/37: added "by flexflex_tac" to compensate for flexflex
451 Pure/goals/gethyps: now calls METAHYPS directly
453 rm-logfiles: no longer mentions directories. WAS
454 rm log {Pure,FOL,ZF,LCF,CTT,LK,Modal,HOL,Cube}/make*.log
455 rm {FOL,ZF,LCF,CTT,LK,Modal,HOL,Cube}/test
456 rm {FOL,ZF,LCF,CTT,LK,Modal,HOL,Cube}/.*.thy.ML
457 rm {FOL,ZF,HOL}/ex/.*.thy.ML
459 MAKE-ALL (Poly/ML) ran perfectly. It took 2:39 hours! (albatross)
461 New version of simp on Isabelle/new -- instantiates unknowns provided only
462 one rule may do so [SINCE REJECTED DUE TO UNPREDICTABLE BEHAVIOR]
464 works with FOLP/ex/nat, but in general could fail in the event of
465 overlapping rewrite rules, since FOLP always instantiates unknowns during
468 ZF: tested with new version
470 HOL: tested with new version, appeared to loop in llist/Lmap_ident
472 **** NEW VERSION OF ASM_SIMP_TAC, WITH METAHYPS ****
474 ZF: failed in perm/comp_mem_injD1: the rule anti_refl_rew is too ambiguous!
475 ZF/wfrec: all uses of wf_ss' require
476 by (METAHYPS (fn hyps => cut_facts_tac hyps 1 THEN
477 SIMP_TAC (wf_ss' addrews (hyps)) 1) 1);
479 ZF/epsilon/eclose_least: changed ASM_SIMP_TAC to SIMP_TAC; this makes
480 METAHYPS version work
482 ZF/arith/add_not_less_self: adds anti_refl_rew
484 ZF/ex/prop-log/hyps_finite: the use of UN_I is very bad -- too undirected.
485 Swapping the premises of UN_I would probably allow instantiation.
487 ZF otherwise seems to work!
489 HOL/llist/llistE: loops! due to rewriting by Rep_LList_LCons of Vars
491 HOL/ex/prop-log/comp_lemma: failed due to uninstantiated Var in
492 (CCONTR_rule RS allI)
498 These overnight runs involve Provers/simp.ML with old treatment of rules
499 (match_tac) and no METAHYPS; they test the new flexflex pairs and
500 discrimination nets, to see whether it runs faster.
502 MAKE-ALL (NJ 0.93) ran perfectly. It took 3:39 hours (4 mins faster)
503 MAKE-ALL (Poly/ML) ran perfectly. It took 3:23 hours (5 mins faster)
505 ZF/simpdata/ZF_ss: deleted anti_refl_rew; non-linear patterns slow down
506 discrimination nets (and this rewrite used only ONCE)
508 ZF/mem_not_refl: new; replaces obsolete anti_refl_rew
510 **Timing experiments**
512 fun HYP_SIMP_TAC ss = METAHYPS (fn hyps => HOL_SIMP_TAC (ss addrews hyps) 1);
514 On large examples such as ...
515 HOL/arith/mod_quo_equality
516 HOL/llist/LListD_implies_ntrunc_equality
517 ZF/ex/bin/integ_of_bin_succ
518 ... it is 1.5 to 3 times faster than ASM_SIMP_TAC. But cannot replace
519 ASM_SIMP_TAC since the auto_tac sometimes fails due to lack of assumptions.
520 If there are few assumptions then HYP_SIMP_TAC is no better.
522 Pure/Makefile: now copies $(ML_DBASE) to $(BIN)/Pure instead of calling
523 make_database, so that users can call make_database for their object-logics.
525 Pure/tctical/SELECT_GOAL: now does nothing if i=1 and there is
530 MAKE-ALL (NJ 0.93) failed in HOL due to lack of disc space.
531 MAKE-ALL (Poly/ML) ran perfectly. It took 3:23 hours
533 **** Installation of new simplifier ****
535 Provers/simp/EXEC: now calls METAHYPS and passes the hyps as an extra arg
538 FOL,HOL/simpdata: auto_tac now handles the hyps argument
540 ZF/simpdata/standard_auto_tac: deleted
541 ZF/simpdata/auto_tac: added hyps argument
542 ZF/epsilon/eclose_least_lemma: no special auto_tac
544 */ex/ROOT: no longer use 'cd' commands; instead pathnames contain "ex/..."
548 MAKE-ALL failed in HOL/Subst
550 HOL/Subst/setplus/cla_case: renamed imp_excluded_middle and simplified.
551 Old version caused ambiguity in rewriting:
552 "[| P ==> P-->Q; ~P ==> ~P-->Q |] ==> Q";
554 **** New tar file placed on /homes/lcp (????) ****
556 Pure/Syntax: improvements to the printing of syntaxes
557 Pure/Syntax/lexicon.ML: added name_of_token
558 Pure/Syntax/earley0A.ML: updated print_gram
562 MAKE-ALL (NJ 0.93) ran perfectly. It took 3:44 hours
563 MAKE-ALL (Poly/ML) failed in HOL due to lack of disc space
565 HOL/list,llist: now share NIL, CONS, List_Fun and List_case
567 make-all: now compresses the log files, which were taking up 4M; this
568 reduces their space by more than 1/3
570 rm-logfiles: now deletes compressed log files.
572 ** Patrick Meche has noted that if the goal is stated with a leading !!
573 quantifier, then the list of premises is always empty -- this gives the
574 effect of an initial (cut_facts_tac prems 1). The final theorem is the
575 same as it would be without the quantifier.
577 ZF: used the point above to simplify many proofs
578 ZF/domrange/cfast_tac: deleted, it simply called cut_facts_tac
582 MAKE-ALL (NJ 0.93) ran perfectly. It took 3:52 hours??
583 MAKE-ALL (Poly/ML) ran perfectly. It took 3:16 hours
587 HOL: installation of finite set notation: {x1,...,xn} (by Tobias Nipkow)
589 HOL/set.thy,set.ML,fun.ML,equalities.ML: addition of rules for "insert",
590 new derivations for "singleton"
592 HOL/llist.thy,llist.ML: changed {x.False} to {}
594 **** New tar file placed on /homes/lcp (584K) ****
598 MAKE-ALL (NJ 0.93) ran out of space in LK.
599 MAKE-ALL (Poly/ML) ran perfectly. It took 3:14 hours
601 Pure/Makefile: inserted "chmod u+w $(BIN)/Pure;" in case $(ML_DBASE) is
606 HOL/list/not_Cons_self: renamed from l_not_Cons_l
607 HOL/list/not_CONS_self: new
609 HOL/llist.thy/Lconst: changed type and def to remove Leaf
610 HOL/llist.ML: changed Lconst theorems
614 MAKE-ALL (Poly/ML) ran perfectly. It took 3:18 hours
616 ** Installation of new HOL from Tobias **
618 HOL/ex/{finite,prop-log} made like the ZF versions
619 HOL/hol.thy: type classes plus, minus, times; overloaded operators + - *
620 HOL/set: set enumeration via "insert"
621 additions to set_cs and set_ss
622 HOL/set,subset,equalities: various lemmas to do with {}, insert and -
623 HOL/llist: One of the proofs needs one fewer commands
624 HOL/arith: many proofs require type constraints due to overloading
626 ** end Installation **
628 ZF/ex/misc: added new lemmas from Abrial's paper
632 HOL/llist.ML/LList_corec_subset1: deleted a fast_tac call; the previous
633 simplification now proves the subgoal.
635 **** New tar file placed on /homes/lcp (584K) ****
637 ** Installation of new simplifier from Tobias **
639 The "case_splits" parameter of SimpFun is moved from the signature to the
640 simpset. SIMP_CASE_TAC and ASM_SIMP_CASE_TAC are removed. The ordinary
641 simplification tactics perform case splits if present in the simpset.
643 The simplifier finds out for itself what constant is affected. Instead of
644 supplying the pair (expand_if,"if"), supply just the rule expand_if.
646 This change affects all calls to SIMP_CASE_TAC and all applications of SimpFun.
648 MAKE-ALL (Poly/ML) ran perfectly. It took 3:18 hours
650 Cube/ex: UNTIL1, UNTIL_THM: replaced by standard tactics DEPTH_SOLVE_1 and
653 HOL: installation of NORM tag for simplication. How was it forgotten??
655 HOL/hol.thy: declaration of NORM
656 HOL/simpdata: NORM_def supplied to SimpFun
660 MAKE-ALL (Poly/ML) ran perfectly. It took 3:33 hours??
664 HOL/prod/Prod_eq: renamed Pair_eq
665 HOL/ex/lex-prod: wf_lex_prod: simplified proof
669 HOL/llist/sumPairE: deleted, thanks to new simplifier's case splits!
673 MAKE-ALL (NJ 0.93) ran out of space in HOL.
674 MAKE-ALL (Poly/ML) failed in HOL.
675 HOL/Subst/utermlemmas/utlemmas_ss: deleted Prod_eq from the congruence rules
679 Pure/logic/flexpair: moved to term, with "equals" etc. Now pervasive
680 Pure/logic/mk_flexpair: now exported
681 Pure/logic/dest_flexpair: new
682 Pure/goals/print_exn: now prints the error message for TERM and TYPE
684 Pure/Syntax/sextension: now =?= has type ['a::{}, 'a] => prop because
685 flexflex pairs can have any type at all. Thus == must have the same type.
687 Pure/thm/flexpair_def: now =?= and == are equated for all 'a::{}.
689 Pure/tctical/equal_abs_elim,equal_abs_elim_list: new (for METAHYPS fix)
690 Pure/tctical/METAHYPS: now works if new proof state has flexflex pairs
692 Pure/Syntax/earley0A,syntax,lexicon: Tokens are represented by strings now,
693 not by integers. (Changed by Tobias)
695 *** Installation of more printing functions ***
697 Pure/sign/sg: changed from a type abbrev to a datatype
698 Pure/type/type_sig: changed from a type abbrev to a datatype
699 These changes needed for abstract type printing in NJ
701 Pure/tctical/print_sg,print_theory: new
703 Pure/drule: new file containing derived rules and printing functions.
704 Mostly from tctical.ML, but includes rewriting rules from tactic.ML.
706 Pure/ROOT: loads drule before tctical; TacticalFun,TacticFun,GoalsFun now
707 depend on Drule and have sharing constraints.
711 Installing new print functions for New Jersey: incompatible with Poly/ML!
713 Pure/NJ/install_pp_nj: new (requires datatypes as above)
714 Pure/POLY/install_pp_nj: a dummy version
716 Pure/ROOT: calls install_pp_nj to install printing for NJ
718 */ROOT: added extra install_pp calls (sg, theory, cterm, typ, ctyp) for
719 Poly/ML [ZF,LCF,Modal do not need them since they inherit them from another
720 logic -- make_database is not used]
724 MAKE-ALL (NJ 0.93) ran perfectly. It took 3:57 hours??
726 Pure/Syntax/lexicon: Yet another leaner and faster version ... (from Tobias)
730 MAKE-ALL (Poly/ML) ran perfectly. It took 3:36 hours
734 ZF/equalities/Union_singleton,Inter_singleton: now refer to {b} instead of
739 HOL/list: Tobias added the [x1,...,xn] notation and the functions hd, tl,
744 MAKE-ALL (Poly/ML) ran perfectly. It took 3:39 hours
746 **** New tar file 92.tar.z placed on /homes/lcp (376K) ****
748 MAKE-ALL (NJ 0.93) ran perfectly. It took 1:49 hours on albatross.
750 Pure/tactic/dres_inst_tac,forw_inst_tac: now call the new
751 make_elim_preserve to preserve Var indexes when creating the elimination
754 ZF/ex/ramsey: modified calls to dres_inst_tac
758 Pure/Thy/read/read_thy,use_thy: the .thy.ML file is now written to the
759 current directory, since the pathname may lead to a non-writeable area.
761 HOL/arith: renamed / and // to div and mod
762 ZF/arith: renamed #/ and #// to div and mod
764 MAKE-ALL (Poly/ML) ran perfectly. It took 1:48 hours on albatross.
766 **** New tar file 92.tar.z placed on /homes/lcp (376K) ****
768 Pure/NJ/commit: new dummy function
769 FOLP/ex/ROOT: inserted commit call to avoid Poly/ML problems
771 make-all: now builds FOLP also!
775 ZF/zf.thy,HOL/list.thy,HOL/set.thy: now constructions involving {_}, [_],
776 <_,_> are formatted as {(_)}, [(_)],
778 MAKE-ALL (Poly/ML) ran perfectly. It took 4:37 hours on muscovy (with FOLP).
780 ZF/Makefile: removed obsolete target for .rules.ML
782 All object-logic Makefiles: EXAMPLES ARE NO LONGER SAVED. This saves disc
783 and avoids problems (in New Jersey ML) of writing to the currently
788 Pure/logic/rewritec: now uses nets for greater speed. Functor LogicFun now
789 takes Net as argument.
791 Pure/ROOT: now loads net before logic.
793 MAKE-ALL (Poly/ML) failed in ZF and HOL.
795 LK/lk.thy: changed constant "not" to "Not" (for consistency with FOL)
799 Pure/tactic/is_letdig: moved to library
800 Pure/Syntax/lexicon/is_qld: deleted, was same as is_letdig
802 MAKE-ALL (Poly/ML) ran perfectly. It took 2:07 hours on albatross.
803 MAKE-ALL (NJ 0.93) ran perfectly. It took 4:41 hours on dunlin.
805 HOL/set/UN1,INT1: new union/intersection operators. Binders UN x.B(x),
808 HOL/univ,llist: now use UN x.B(x) instead of Union(range(B))
810 HOL/subset: added lattice properties for INT, UN (both forms)
814 MAKE-ALL (NJ 0.93) ran perfectly. It took 4:45 hours on dunlin.
816 **** New tar file 92.tar.z placed on /homes/lcp (384K) ****
820 HOL/list.thy/List_rec_def: changed pred_sexp (a variable!) to pred_Sexp.
821 Using def_wfrec hides such errors!!
823 **** New tar file 92.tar.gz placed on /homes/lcp (384K) ****
825 ** NEW VERSION FROM MUNICH WITH ==-REWRITING **
827 ** The following changes are Toby's **
831 Renamed mark_free to freeze_vars and thaw_tvars to thaw_vars.
832 Added both functions to the signature.
836 Added val subsig: sg * sg -> bool to signature.
837 Added trueprop :: prop and mark_prop : prop => prop to pure_sg.
841 val freeze_vars: term -> term
842 val thaw_vars: term -> term
843 val strip_all_imp: term * int -> term list * term * int
845 Moved rewritec_bottom and rewritec_top to thm.ML.
846 Only bottom-up rewriting supported any longer.
852 (* internal form of conditional ==-rewrite rules *)
854 val add_mss: meta_simpset * thm list -> meta_simpset
855 val empty_mss: meta_simpset
856 val mk_mss: thm list -> meta_simpset
858 val mark_prop_def: thm
860 val trueprop_def: thm
862 (* bottom-up conditional ==-rewriting with local ==>-assumptions *)
863 val rewrite_cterm: meta_simpset -> (thm -> thm list)
864 -> (meta_simpset -> thm list -> Sign.cterm -> thm)
866 val trace_simp: bool ref
868 Simplified concl_of: call to Logic.skip_flexpairs redundant.
875 val asm_rewrite_rule: (thm -> thm list) -> thm list -> thm -> thm
876 val rewrite_goal_rule: (thm -> thm list) -> thm list -> int -> thm -> thm
877 val rewrite_goals_rule: (thm -> thm list) -> thm list -> thm -> thm
879 (* derived concepts *)
880 val forall_trueprop_eq: thm
881 val implies_trueprop_eq: thm
882 val mk_trueprop_eq: thm -> thm
883 val reflexive_eq: thm
884 val reflexive_thm: thm
885 val trueprop_implies_eq: thm
886 val thm_implies: thm -> thm -> thm
887 val thm_equals: thm -> thm -> thm
889 (*Moved here from tactic.ML:*)
898 val asm_rewrite_goal_tac: (thm -> thm list) -> thm list -> int -> tactic
899 val asm_rewrite_goals_tac: (thm -> thm list) -> thm list -> tactic
900 val asm_rewrite_tac: (thm -> thm list) -> thm list -> tactic
901 val fold_goal_tac: thm list -> int -> tactic
902 val rewrite_goal_tac: thm list -> int -> tactic
911 Changed prepare_proof to make sure that rewriting with empty list of
912 meta-thms is identity.
914 ** End of Toby's changes **
918 Pure/sign/typ_of,read_ctyp: new
919 Pure/logic/dest_flexpair: now exported
921 Pure/drule/flexpair_intr,flexpair_elim: new; fixes a bug in
922 flexpair_abs_elim_list
924 HOL/equalities/image_empty,image_insert: new
925 HOL/ex/finite/Fin_imageI: new
927 Installed Martin Coen's CCL as new object-logic
931 ** More changes from Munich (Markus Wenzel) **
933 Pure/library: added the, is_some, is_none, separate and improved space_implode
934 Pure/sign: Sign.extend now calls Syntax.extend with list of constants
935 Pure/symtab: added is_null
936 Pure/Syntax/sextension: added empty_sext
937 Pure/Syntax/syntax: changed Syntax.extend for compatibility with future version
939 HOL now exceeds poly's default heap size. Hence HOL/Makefile needs to
942 HOL/univ/ntrunc_subsetD, etc: deleted the useless j<k assumption
946 MAKE-ALL (Poly/ML) ran perfectly. It took 4:59 hours on dunlin (with CCL).
948 Pure/sign/read_def_cterm: now prints the offending terms, as well as the
949 types, when exception TYPE is raised.
951 HOL/llist: some tidying
955 HOL/llist/Lconst_type: generalized from Lconst(M): LList({M})
959 MAKE-ALL (Poly/ML) ran perfectly. It took 2:23 hours on albatross (with CCL)
961 MAKE-ALL (NJ 0.93) failed in CCL due to use of "abstraction" as an
964 **** New tar file 92.tar.gz placed on /homes/lcp (384K) **** (with CCL)
966 CCL/ROOT: added ".ML" extension to use commands for NJ compatibility
970 MAKE-ALL (Poly/ML) ran perfectly. It took 2:23 hours on albatross.
971 MAKE-ALL (NJ 0.93) failed in HOL due to lack of ".ML" extension
973 HOL/fun/rangeE,imageE: eta-expanded f to get variable name preservation
975 HOL/llist/iterates_equality,lmap_lappend_distrib: tidied
979 HOL/set/UN1_I: made the Var and Bound variables agree ("x") to get variable
982 HOL/llist: co-induction rules applied with res_inst_tac to state the
983 bisimulation directly
987 MAKE-ALL (NJ 0.93) ran perfectly. It took 2:10 hours on albatross.
988 MAKE-ALL (Poly/ML) ran perfectly. It took 2:23 hours on albatross.
990 92/Makefile/$(BIN)/Pure: changed echo makefile= to echo database=
992 **** New tar file 92.tar.gz placed on /homes/lcp (424K) **** (with CCL)
995 ** NEW VERSION FROM MUNICH WITH ABSTRACT SYNTAX TREES & NEW PARSER **
997 I have merged in the changes shown above since 24 June
999 CHANGES LOG OF Markus Wenzel (MMW)
1003 *** Beta release of new syntax module ***
1004 (should be 99% backwards compatible)
1007 added keywords for "translations" section
1011 added syntax for "translations" section
1012 .*.thy.ML files now human readable
1013 .*.thy.ML used to be generated incorrectly if no mixfix but "ML" section
1014 "ML" section no longer demands any definitions (parse_translation, ...)
1017 read_thy: added close_in
1018 added file_exists (not perfect)
1019 use_thy: now uses file_exists
1022 added syn_of: theory -> syntax
1025 SYNTAX_FILES: added Syntax/ast.ML
1027 Pure/Syntax/pretty.ML
1028 added str_of: T -> string
1033 Pure/Syntax/extension.ML
1034 Pure/Syntax/parse_tree.ML
1035 Pure/Syntax/printer.ML
1037 Pure/Syntax/sextension.ML
1038 Pure/Syntax/syntax.ML
1039 Pure/Syntax/type_ext.ML
1040 Pure/Syntax/xgram.ML
1041 These files have been completely rewritten, though the global structure
1042 is similar to the old one.
1046 New versions of HOL and Cube: use translation rules wherever possible;
1050 removed alt_tr', mk_bindopt_tr'
1051 alternative binders now implemented via translation rules and mk_alt_ast_tr'
1055 removed type "finset"
1056 now uses category "args" for finite sets
1058 added "translations" section
1062 removed type "listenum"
1063 now uses category "args" for lists
1065 added "translations" section
1069 changed indentation of Lam and Pi from 2 to 3
1070 removed qnt_tr, qnt_tr', no_asms_tr, no_asms_tr'
1071 fixed fun_tr': all but one newly introduced frees will have type dummyT
1072 added "translations" section
1075 30-Jun-1993, 05-Jul-1993 MMW
1076 Improved toplevel pretty printers:
1077 - unified interface for POLY and NJ;
1078 - print functions now insert atomic string into the toplevel's pp stream,
1079 rather than writing it to std_out (advantage: output appears at the
1080 correct position, disadvantage: output cannot be broken);
1081 (Is there anybody in this universe who exactly knows how Poly's install_pp
1082 is supposed to work?);
1085 removed dummy install_pp
1086 added make_pp, install_pp
1089 removed dummy install_pp_nj
1093 removed install_pp_nj stuff
1096 added str_of_sg, str_of_theory, str_of_thm
1102 added str_of_term, str_of_typ, str_of_cterm, str_of_ctyp
1105 added str_of_term, str_of_typ
1113 replaced install_pp stuff by 'use "../Pure/install_pp.ML"'
1121 added ".ML" suffix to some filenames
1124 replaced HOL_Rule.thy by HOL.thy
1127 quit was incorrectly int -> unit
1131 Pure/Syntax/sextension/eta_contract: now initially false
1133 Pure/library/cat_lines: no longer calls "distinct"
1134 Pure/sign: replaced to calls of implode (map (apr(op^,"\n") o ... by cat_lines
1135 NB This could cause duplicate error messages from Pure/sign and Pure/type
1137 Pure/goals/prove_goalw: now prints some of the information from print_exn
1141 MAKE-ALL (Poly/ML) ran perfectly. It took 2:26 hours on albatross.
1143 **** New tar file 93.tar.gz placed on /homes/lcp (480K) ****
1147 MAKE-ALL (NJ 0.93) ran perfectly. It took 2:13 hours on albatross.
1148 MAKE-ALL (Poly/ML) ran perfectly. It took 2:25 hours on albatross.
1152 ZF/zf.thy: new version from Marcus Wenzel
1154 ZF: ** installation of inductive definitions **
1156 changing the argument order of "split"; affects fst/snd too
1157 sum.thy zf.thy ex/bin.thy ex/integ.thy ex/simult.thy ex/term.thy
1160 changing the argument order of "case" and adding "Part": sum.thy sum.ML
1162 ZF/zf.ML/rev_subsetD,rev_bspec: new
1164 ZF/mono: new rules for implication
1165 ZF/mono/Collect_mono: now for use with implication rules
1167 ZF/zf.ML/ballE': renamed rev_ballE
1169 ZF/list.thy,list.ML: files renamed list-fn.thy, list-fn.ML
1170 ZF/list.ML: new version simply holds the datatype definition
1171 NB THE LIST CONSTRUCTORS ARE NOW Nil/Cons, not 0/Pair.
1173 ZF/extend_ind.ML, datatype.ML: new files
1174 ZF/fin.ML: moved from ex/finite.ML
1178 ZF/ex/sexp: deleted this example -- it seems hardly worth the trouble of
1181 ZF/ex/bt.thy,bt.ML: files renamed bt-fn.thy, bt-fn.ML
1182 ZF/ex/bt.ML: new version simply holds the datatype definition
1184 ZF/ex/term.thy,term.ML: files renamed term-fn.thy, term-fn.ML
1185 ZF/ex/term.ML: new version simply holds the datatype definition
1187 ZF/sum/InlI,InrI: renamed from sum_InlI, sum_InlI
1191 ZF/univ/rank_ss: new, for proving recursion equations
1193 ZF/domrange/image_iff,image_singleton_iff,vimage_iff,vimage_singleton_iff,
1196 ZF/domrange/field_subset: modified
1198 ZF/list/list_cases: no longer proved by induction!
1199 ZF/wf/wf_trancl: simplified proof
1201 ZF/equalities: new laws for field
1205 ZF/trancl/trancl_induct: new
1206 ZF/trancl/rtrancl_induct,trancl_induct: now with more type information
1208 ** More changes from Munich (Markus Wenzel) **
1210 Update of new syntax module (aka macro system): mostly internal cleanup and
1215 added Syntax.print_gram, Syntax.print_trans, Syntax.print_syntax
1216 cleaned type and Pure syntax: "_CLASSES" -> "classes", "_SORTS" -> "sorts",
1217 "_==>" -> "==>", "_fun" -> "fun", added some space for printing
1218 Printer: partial fix of the "PROP <aprop>" problem: print "PROP " before
1219 any Var or Free of type propT
1220 Syntax: added ndependent_tr, dependent_tr'
1222 Pure/sign.ML: removed declaration of "==>" (now in Syntax.pure_sext)
1224 Changes to object logics: minor cleanups and replacement of most remaining ML
1225 translations by rewrite rules (see also file "Translations");
1228 added "translations" section
1229 removed all parse/print translations except ndependent_tr, dependent_tr'
1230 fixed dependent_tr': all but one newly introduced frees have type dummyT
1231 replaced id by idt in order to make terms rereadable if !show_types
1235 replaced fun_tr/tr' by ndependent_tr/dependent_tr'
1238 added translations rules for PROD and SUM
1239 removed dependent_tr
1240 removed definitions of ndependent_tr, dependent_tr'
1242 HOL/set.thy: replaced id by idt
1244 CCL/ROOT.ML: Logtic -> Logic
1247 added "translations" section
1248 removed "ML" section
1252 added "translations" section
1253 removed definitions of ndependent_tr, dependent_tr'
1256 Yet another improvement of toplevel pretty printers: output now breakable;
1258 Pure/NJ.ML Pure/POLY.ML improved make_pp
1260 Pure/install_pp.ML: replaced str_of_* by pprint_*
1262 Pure/drule.ML: replaced str_of_{sg,theory,thm} by pprint_*
1264 Pure/sign.ML: replaced str_of_{term,typ,cterm,ctyp} by pprint_*
1266 Pure/goals.ML: fixed and replaced str_of_{term,typ} by pprint_*
1268 Pure/Syntax/pretty.ML: added pprint, quote
1270 Minor changes and additions;
1272 Pure/sign.ML: renamed stamp "PURE" to "Pure"
1275 added quote: string -> string
1276 added to_lower: string -> bool
1278 Pure/NJ.ML,POLY.ML: added file_info of Carsten Clasohm
1282 MAKE-ALL (Poly/ML) ran perfectly.
1284 Pure/goals/print_sign_exn: new, takes most code from print_exn
1285 Pure/goals/prove_goalw: displays exceptions using print_sign_exn
1287 Pure/drule/print_sg: now calls pretty_sg to agree with pprint_sg
1289 Pure/library,...: replaced front/nth_tail by take/drop.
1291 Pure/term/typ_tfrees,typ_tvars,term_tfrees,term_tvars: new
1292 thm/mk_rew_triple, drule/types_sorts, sign/zero_tvar_indices: now use the above
1294 Pure/logic/add_term_vars,add_term_frees,insert_aterm,atless:
1295 moved to term, joining similar functions for type variables;
1296 Logic.vars and Logic.frees are now term_vars and term_frees
1298 Pure/term/subst_free: new
1300 Pure/tactic/is_fact: newly exported
1302 Provers/simp/mk_congs: uses filter_out is_fact to delete trivial cong rules
1304 Pure/tactic/rename_last_tac: now uses Syntax.is_identifier instead of
1307 **** New tar file 93.tar.gz placed on /homes/lcp (448K) ****
1311 MAKE-ALL (NJ 0.93) failed in ZF due to Compiler bug: elabDecl:open:FctBodyStr
1312 MAKE-ALL (Poly/ML) failed in ZF/enum. It took 2:33 hours on albatross.
1314 Pure/drule/triv_forall_equality: new
1315 Pure/tactic/prune_params_tac: new
1317 Provers/hypsubst/bound_hyp_subst_tac: new, safer than hyp_subst_tac
1321 Pure/tactic/rule_by_tactic: new
1323 ZF/perm/compEpair: now proved via rule_by_tactic
1325 ZF/extend_ind/cases,mk_cases: new
1326 ZF/datatype/mk_free: new
1327 ZF/list: now calls List.mk_cases
1331 Provers/slow_tac,slow_best_tac: new
1335 MAKE-ALL (Poly/ML) failed in ZF
1337 ZF/sum/sumE2: deleted since unused
1338 ZF/sum/sum_iff,sum_subset_iff,sum_equal_iff: new
1339 ZF/univ/Transset_Vfrom: new; used in proof of Transset_Vset
1343 Pure/goals/prepare_proof: after "Additional hypotheses", now actually
1346 ZF/ordinal/Transset_Union_family, Transset_Inter_family: renamed from
1347 Transset_Union, Transset_Inter
1349 ZF/ordinal/Transset_Union: new
1350 ZF/univ/pair_in_univ: renamed Pair_in_univ
1352 ZF/mono/product_mono: generalized to Sigma_mono; changed uses in trancl, univ
1354 ZF/lfp/lfp_Tarski,def_lfp_Tarski: renamed from Tarski,def_Tarski; changed
1355 uses in extend_ind.ML, nat.ML, trancl.ML.
1357 ZF/ex/misc: Schroeder-Bernstein Theorem moved here from lfp.ML
1359 ZF/fixedpt.thy,.ML: renamed from lfp.thy,.ML, and gfp added
1363 ZF/zf.thy/ndependent_tr,dependent_tr': deleted, since they are now on
1368 Pure/library.ML: added functions
1369 assocs: (''a * 'b list) list -> ''a -> 'b list
1370 transitive_closure: (''a * ''a list) list -> (''a * ''a list) list
1372 Pure/type.ML: deleted (inefficient) transitive_closure