edits.txt
author paulson
Tue Jul 09 23:05:26 2002 +0200 (2002-07-09)
changeset 13328 703de709a64b
parent 0 a5a9c433f639
permissions -rw-r--r--
better document preparation
     1 EDITS TO THE ISABELLE SYSTEM FOR 1993
     2 
     3 11 January 
     4 
     5 */README: Eliminated references to Makefile.NJ, which no longer exists.
     6 
     7 **** New tar file placed on /homes/lcp (464K) **** 
     8 
     9 14 January
    10 
    11 Provers/simp/pr_goal_lhs: now distinct from pr_goal_concl so that tracing
    12 prints conditions correctly.
    13 
    14 {CTT/arith,HOL/ex/arith/ZF/arith}/add_mult_distrib: renamed from
    15 add_mult_dist, to agree with the other _distrib rules
    16 
    17 20 January
    18 
    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
    21 
    22 21 January
    23 
    24 {CTT/arith,HOL/ex/arith/ZF/arith}/add_inverse_diff: renamed to add_diff_inverse
    25 
    26 22 January
    27 
    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
    31 
    32 ZF/bool/boolI0,boolI1: renamed as bool_0I, bool_1I
    33 
    34 25 January
    35 
    36 MAKE-ALL (NJ 0.75) ran perfectly.  It took 3:19 hours!?
    37 
    38 ZF/bool/not,and,or,xor: new
    39 
    40 27 January
    41 
    42 ZF/ex/bin: new theory of binary integer arithmetic
    43 
    44 27 January
    45 
    46 MAKE-ALL (Poly/ML) ran perfectly.  It took 6:33 hours???
    47 (ZF took almost 5 hours!)
    48 
    49 **** New tar file placed on /homes/lcp (472K) **** 
    50 
    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
    54 
    55 29 January
    56 
    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
    61 
    62 2 February
    63 
    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.
    67 
    68 Pure/Thy/scan/comment: renamed from komt
    69 Pure/Thy/scan/numeric: renamed from zahl
    70 
    71 Pure/Syntax/syntax,lexicon,type_ext,extension,sextension: modified by
    72 Tobias to change ID, TVAR, ... to lower case.
    73 
    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
    76 
    77 3 February
    78 
    79 MAKE-ALL (Poly/ML) ran perfectly.  It took 2:50 hours.
    80 
    81 4 February
    82 
    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
    85 
    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)) \
    89     \    |] ==> P(s)";
    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));
    93     val sumE = result();
    94 
    95 8 February
    96 
    97 Changes from Tobias:
    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
   100 
   101 9 February
   102 
   103 HOL/ex/arith: moved to main HOL directory
   104 HOL/prod: now define the type "unit" and constant "(): unit"
   105 
   106 11 February
   107 
   108 HOL/arith: eliminated redefinitions of nat_ss and arith_ss
   109 
   110 12 February
   111 
   112 MAKE-ALL (Poly/ML) ran perfectly.  It took 2:50 hours.
   113 
   114 Pure/Thy/scan/string: now correctly recognizes ML-style strings.
   115 
   116 15 February
   117 
   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)
   121 
   122 **** New tar file placed on /homes/lcp (480K) **** 
   123 
   124 18 February
   125 
   126 Pure/Syntax/earley0A/compile_xgram: Tobias deleted the third argument, as
   127 it was unused.
   128 
   129 Pure/Syntax/earley0A: modified accordingly.
   130 
   131 19 February
   132 
   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
   135 
   136 **** New tar file placed on /homes/lcp (480K) **** 
   137 
   138 20 February
   139 
   140 MAKE-ALL (NJ 0.93) ran perfectly.  It took 3:30 hours 
   141 
   142 10 March
   143 
   144 HOL/fun/image_eqI: fixed bad pattern
   145 
   146 11 March
   147 
   148 MAKE-ALL (Poly/ML) failed in HOL!
   149 
   150 HOL/fun: moved "mono" proofs to HOL/subset, since they rely on subset laws
   151 of Int and Un.
   152 
   153 12 March
   154 
   155 ZF/ex/misc: new example from Bledsoe
   156 
   157 15 March
   158 
   159 ZF/perm: two new theorems inspired by Pastre
   160 
   161 16 March
   162 
   163 Weakened congruence rules for HOL: speeds simplification considerably by
   164 NOT simplifying the body of a conditional or eliminator.
   165 
   166 HOL/simpdata/mk_weak_congs: new, to make weakened congruence rules
   167 
   168 HOL/simpdata/congs: renamed HOL_congs and weakened the "if" rule
   169 
   170 HOL/simpdata/HOL_congs: now contains polymorphic rules for the overloaded
   171 operators < and <=
   172 
   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
   177 
   178 HOL & test rebuilt perfectly
   179 
   180 Pure/goals/prepare_proof/mkresult: fixed bug in signature check.  Now
   181 compares the FINAL signature with that from the original theory.
   182 
   183 Pure/goals/prepare_proof: ensures that [prove_]goalw checks that the
   184 definitions do not update the proof state.
   185 
   186 17 March
   187 
   188 MAKE-ALL (Poly/ML) ran perfectly.
   189 
   190 18 March
   191 
   192 MAKE-ALL (Poly/ML) failed in HOL/ex/Substitutions
   193 
   194 HOL/ex/Subst/setplus: changed Set.thy to Setplus.thy where
   195 necessary
   196 
   197 ZF/perm: proved some rules about inj and surj
   198 
   199 ZF/ex/misc: did some of Pastre's examples
   200 
   201 Pure/library/gen_ins,gen_union: new
   202 
   203 HOL/ex/Subst/subst: renamed rangeE to srangeE
   204 
   205 18 March
   206 
   207 MAKE-ALL (Poly/ML) failed in HOL/ex/term due to renaming of list_ss in
   208 ex/Subst/alist
   209 
   210 HOL/list/list_congs: new; re-organized simpsets a bit
   211 
   212 Pure/goals/sign_error: new
   213 
   214 Pure/goals/prepare_proof,by_com: now print the list of new theories when
   215 the signature of the proof state changes 
   216 
   217 HOL/prod,sexp: renamed fst, snd to fst_conv, snd_conv to avoid over-writing
   218 the library functions fst, snd
   219 
   220 HOL/fun/image_compose: new
   221 
   222 21 March
   223 
   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
   227 
   228 **** New tar file placed on /homes/lcp (504K) **** 
   229 
   230 ZF/pair,simpdata: renamed fst, snd to fst_conv, snd_conv to avoid over-writing
   231 the library functions fst, snd
   232 
   233 HOL/prod/prod_fun_imageI,E: new
   234 
   235 HOL/ex/Subst/Unify: renamed to Unifier to avoid clobbering structure Unify
   236 of Pure
   237 
   238 24 March
   239 
   240 HOL/trancl/comp_subset_Sigma: new
   241 HOL/wf/wfI: new
   242 
   243 HOL/Subst: moved from HOL/ex/Subst to shorten pathnames
   244 HOL/Makefile: target 'test' now loads Subst/ROOT separately
   245 
   246 *** Installation of gfp, coinduction, ... to HOL ***
   247 
   248 HOL/gfp,llist: new
   249 HOL/univ,sexp,list: replaced with new version
   250 
   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.
   256 
   257 25 March
   258 
   259 Pure/thm: renamed 'bires' to 'eres' in many places (not exported) --
   260 biresolution now refers to resolution with (flag,rule) pairs.
   261 
   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:
   265 
   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;
   268     val l1 = result();
   269 
   270     val rls = [refl] RL [bexI] RL [l1];
   271 
   272     goal Set.thy "True = False";
   273     brs rls 1; br singletonI 1;
   274     result();
   275 
   276 Marcus Moore noted that the error only occurred with
   277 Logic.auto_rename:=false.  Elements of the fix:
   278 
   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
   281 Vars in tpairs.
   282 
   283 2.  bicompose_aux/tryasms and res now unpack the "cell" and supply its tpairs
   284 to newAs.
   285 
   286 HOL/lfp,gfp,ex/set: renamed Tarski to lfp_Tarski
   287 
   288 HOL/lfp,list,llist,nat,sexp,trancl,Subst/uterm,ex/simult,ex/term: renamed
   289 def_Tarski to def_lfp_Tarski 
   290 
   291 26 March
   292 
   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)
   295 
   296 Pure/Thy/scan/is_digit,is_letter: deleted.  They are already in
   297 Pure/library, and these versions used non-Standard string comparisons!
   298 
   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. 
   303 
   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
   307 
   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
   311 
   312 29 March
   313 
   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!
   316 
   317 **** New tar file placed on /homes/lcp (518K) **** 
   318 
   319 30 March
   320 
   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.
   323 
   324 8 April
   325 
   326 MAKE-ALL (Poly/ML) ran perfectly.  It took 3:49 hours!
   327 
   328 **** New tar file placed on /homes/lcp (520K) **** 
   329 
   330 **** Updates for pattern unification (Tobias Nipkow) ****
   331 
   332 Pure/pattern.ML: new, pattern unification
   333 
   334 Pure/Makefile and ROOT.ML: included pattern.ML
   335 
   336 Pure/library.ML: added predicate downto0
   337 
   338 Pure/unify.ML: call pattern unification first. Removed call to could_unify.
   339 
   340 FOL/Makefile/FILES: now mentions ifol.ML (previously repeated fol.ML instead)
   341 
   342 **** Installation of Martin Coen's FOLP (FOL + proof objects) ****
   343 
   344 renamed PFOL, PIFOL to FOLP, IFOLP, etc.
   345 
   346 9 April
   347 
   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!
   350 
   351 **** New tar file placed on /homes/lcp (576K) **** 
   352 
   353 **** Installation of Discrimination Nets ****
   354 
   355 *Affected files (those mentioning Stringtree, compat_thms or rtr_resolve_tac)
   356 Pure/ROOT.ML,goals.ML,stringtree.ML,tactic.ML
   357 Provers/simp.ML
   358 HOL/ex/meson.ML
   359 
   360 *Affected files (those mentioning compat_resolve_tac)
   361 Pure/tactic.ML
   362 Provers/typedsimp.ML
   363 CTT/ctt.ML
   364 
   365 Pure/stringtree: saved on Isabelle/old
   366 Pure/net: new
   367 Pure/Makefile/FILES: now mentions net.ML, not stringtree.ML
   368 Pure/ROOT: now mentions net.ML, not stringtree.ML
   369 
   370 Pure/goals/compat_goal: DELETED
   371 
   372 Pure/tactic/compat_thms,rtr_resolve_tac,compat_resolve_tac,insert_thm,
   373 delete_thm,head_string: DELETED
   374 
   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
   378 
   379 Pure/tactic/filt_resolve_tac: new implementation using nets!
   380 
   381 Provers/simp: replaced by new version
   382 
   383 Provers/typedsimp: changed compat_resolve_tac to filt_resolve_tac and
   384 updated comments
   385 
   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
   388 
   389 CTT tested
   390 
   391 HOL/ex/meson/ins_term,has_reps: replaced Stringtree by Net
   392 
   393 FOL tested
   394 
   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
   397 
   398 ZF/ex/bin/integ_of_bin_type: proof required reordering of rules --
   399 typechk_tac now respects this ordering!
   400 
   401 ZF tested
   402 
   403 DOCUMENTATION
   404 
   405 Logics/CTT: Removed mention of compat_resolve_tac 
   406 Ref/goals: deleted compat_goal's entry
   407 
   408 Provers/hypsubst/lasthyp_subst_tac: deleted
   409 
   410 FOLP/ROOT/dest_eq: corrected; now hyp_subst_tac works!
   411 
   412 12 April
   413 
   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!
   416 
   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 
   420 
   421 {FOL,FOLP}/int-prover/safe_brls: removed (asm_rl,true) since assume_tac is
   422 used explicitly!!
   423 
   424 FOLP/ifolp/uniq_assume_tac: new, since eq_assume_tac is almost useless
   425 
   426 FOLP/{int-prover,classical}/uniq_mp_tac: replace eq_mp_tac and call
   427 uniq_assume_tac
   428 
   429 Provers/classical: REPLACED BY 'NET' VERSION!
   430 
   431 13 April
   432 
   433 MAKE-ALL (Poly/ML) failed in ZF and ran out of quota for Cube.
   434 
   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
   439 rigid!
   440 
   441 unify/CHANGE_FAIL: new, for flexible occurrence of bound variable
   442 unify/change_bnos: now takes "flex" as argument, indicating path status
   443 
   444 14 April
   445 
   446 MAKE-ALL (Poly/ML) failed in HOL (ASM_SIMP_TAC redefined!) and LK
   447 
   448 LK/ex/hard-quant/37: added "by flexflex_tac" to compensate for flexflex
   449 changes
   450 
   451 Pure/goals/gethyps: now calls METAHYPS directly
   452 
   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
   458 
   459 MAKE-ALL (Poly/ML) ran perfectly.  It took 2:39 hours! (albatross)
   460 
   461 New version of simp on Isabelle/new -- instantiates unknowns provided only
   462 one rule may do so [SINCE REJECTED DUE TO UNPREDICTABLE BEHAVIOR]
   463 
   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
   466 rewriting.
   467 
   468 ZF: tested with new version
   469 
   470 HOL: tested with new version, appeared to loop in llist/Lmap_ident
   471 
   472 **** NEW VERSION OF ASM_SIMP_TAC, WITH METAHYPS ****
   473 
   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);
   478 
   479 ZF/epsilon/eclose_least: changed ASM_SIMP_TAC to SIMP_TAC; this makes
   480 METAHYPS version work
   481 
   482 ZF/arith/add_not_less_self: adds anti_refl_rew
   483 
   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.
   486 
   487 ZF otherwise seems to work!
   488 
   489 HOL/llist/llistE: loops! due to rewriting by Rep_LList_LCons of Vars
   490 
   491 HOL/ex/prop-log/comp_lemma: failed due to uninstantiated Var in 
   492 (CCONTR_rule RS allI)
   493 
   494 *** REJECTED
   495 
   496 15 April
   497 
   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.
   501 
   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)
   504 
   505 ZF/simpdata/ZF_ss: deleted anti_refl_rew; non-linear patterns slow down
   506 discrimination nets (and this rewrite used only ONCE)
   507 
   508 ZF/mem_not_refl: new; replaces obsolete anti_refl_rew
   509 
   510 **Timing experiments**
   511 
   512 fun HYP_SIMP_TAC ss = METAHYPS (fn hyps => HOL_SIMP_TAC (ss addrews hyps) 1);
   513 
   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.
   521 
   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.
   524 
   525 Pure/tctical/SELECT_GOAL: now does nothing if i=1 and there is
   526 only one subgoal.
   527 
   528 19 April
   529 
   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 
   532 
   533 **** Installation of new simplifier ****
   534 
   535 Provers/simp/EXEC: now calls METAHYPS and passes the hyps as an extra arg
   536 to the auto_tac.
   537 
   538 FOL,HOL/simpdata: auto_tac now handles the hyps argument
   539 
   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 
   543 
   544 */ex/ROOT: no longer use 'cd' commands; instead pathnames contain "ex/..."
   545 
   546 20 April
   547 
   548 MAKE-ALL failed in HOL/Subst
   549 
   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";
   553 
   554 **** New tar file placed on /homes/lcp (????) **** 
   555 
   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
   559 
   560 21 April
   561 
   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
   564 
   565 HOL/list,llist: now share NIL, CONS, List_Fun and List_case
   566 
   567 make-all: now compresses the log files, which were taking up 4M; this
   568 reduces their space by more than 1/3
   569 
   570 rm-logfiles: now deletes compressed log files.
   571 
   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.
   576 
   577 ZF: used the point above to simplify many proofs
   578 ZF/domrange/cfast_tac: deleted, it simply called cut_facts_tac
   579 
   580 22 April
   581 
   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
   584 
   585 30 April
   586 
   587 HOL: installation of finite set notation: {x1,...,xn} (by Tobias Nipkow)
   588 
   589 HOL/set.thy,set.ML,fun.ML,equalities.ML: addition of rules for "insert",
   590 new derivations for "singleton"
   591 
   592 HOL/llist.thy,llist.ML: changed {x.False} to {}
   593 
   594 **** New tar file placed on /homes/lcp (584K) **** 
   595 
   596 4 May
   597 
   598 MAKE-ALL (NJ 0.93) ran out of space in LK.
   599 MAKE-ALL (Poly/ML) ran perfectly.  It took 3:14 hours
   600 
   601 Pure/Makefile: inserted "chmod u+w $(BIN)/Pure;" in case $(ML_DBASE) is
   602 write-protected
   603 
   604 5 May
   605 
   606 HOL/list/not_Cons_self: renamed from l_not_Cons_l
   607 HOL/list/not_CONS_self: new
   608 
   609 HOL/llist.thy/Lconst: changed type and def to remove Leaf
   610 HOL/llist.ML: changed Lconst theorems
   611 
   612 6 May
   613 
   614 MAKE-ALL (Poly/ML) ran perfectly.  It took 3:18 hours
   615 
   616 ** Installation of new HOL from Tobias **
   617 
   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
   625 
   626 ** end Installation **
   627 
   628 ZF/ex/misc: added new lemmas from Abrial's paper
   629 
   630 7 May 
   631 
   632 HOL/llist.ML/LList_corec_subset1: deleted a fast_tac call; the previous
   633 simplification now proves the subgoal.
   634 
   635 **** New tar file placed on /homes/lcp (584K) **** 
   636 
   637 ** Installation of new simplifier from Tobias **
   638 
   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.
   642 
   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.
   645 
   646 This change affects all calls to SIMP_CASE_TAC and all applications of SimpFun.
   647 
   648 MAKE-ALL (Poly/ML) ran perfectly.  It took 3:18 hours
   649 
   650 Cube/ex: UNTIL1, UNTIL_THM: replaced by standard tactics DEPTH_SOLVE_1 and
   651 DEPTH_SOLVE
   652 
   653 HOL: installation of NORM tag for simplication.  How was it forgotten??
   654 
   655 HOL/hol.thy: declaration of NORM
   656 HOL/simpdata: NORM_def supplied to SimpFun
   657 
   658 10 May
   659 
   660 MAKE-ALL (Poly/ML) ran perfectly.  It took 3:33 hours??
   661 
   662 11 May
   663 
   664 HOL/prod/Prod_eq: renamed Pair_eq
   665 HOL/ex/lex-prod: wf_lex_prod: simplified proof
   666 
   667 HOL/fun/inj_eq: new
   668 
   669 HOL/llist/sumPairE: deleted, thanks to new simplifier's case splits!
   670 
   671 12 May
   672 
   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
   676 
   677 13 May
   678 
   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
   683 
   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.
   686 
   687 Pure/thm/flexpair_def: now =?= and == are equated for all 'a::{}.
   688 
   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
   691 
   692 Pure/Syntax/earley0A,syntax,lexicon: Tokens are represented by strings now,
   693 not by integers.  (Changed by Tobias)
   694 
   695 *** Installation of more printing functions ***
   696 
   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
   700 
   701 Pure/tctical/print_sg,print_theory: new
   702 
   703 Pure/drule: new file containing derived rules and printing functions.
   704 Mostly from tctical.ML, but includes rewriting rules from tactic.ML.
   705 
   706 Pure/ROOT: loads drule before tctical; TacticalFun,TacticFun,GoalsFun now
   707 depend on Drule and have sharing constraints.
   708 
   709 14 May
   710 
   711 Installing new print functions for New Jersey: incompatible with Poly/ML!
   712 
   713 Pure/NJ/install_pp_nj: new (requires datatypes as above)
   714 Pure/POLY/install_pp_nj: a dummy version
   715 
   716 Pure/ROOT: calls install_pp_nj to install printing for NJ
   717 
   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]
   721 
   722 17 May
   723 
   724 MAKE-ALL (NJ 0.93) ran perfectly.  It took 3:57 hours??
   725 
   726 Pure/Syntax/lexicon: Yet another leaner and faster version ... (from Tobias)
   727 
   728 18 May
   729 
   730 MAKE-ALL (Poly/ML) ran perfectly.  It took 3:36 hours
   731 
   732 19 May
   733 
   734 ZF/equalities/Union_singleton,Inter_singleton: now refer to {b} instead of
   735 complex assumptions
   736 
   737 20 May
   738 
   739 HOL/list: Tobias added the [x1,...,xn] notation and the functions hd, tl,
   740 null and list_case.
   741 
   742 1 June
   743 
   744 MAKE-ALL (Poly/ML) ran perfectly.  It took 3:39 hours
   745 
   746 **** New tar file 92.tar.z placed on /homes/lcp (376K) **** 
   747 
   748 MAKE-ALL (NJ 0.93) ran perfectly.  It took 1:49 hours on albatross.
   749 
   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
   752 rule.
   753 
   754 ZF/ex/ramsey: modified calls to dres_inst_tac
   755 
   756 2 June
   757 
   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.
   760 
   761 HOL/arith: renamed / and // to div and mod
   762 ZF/arith: renamed #/ and #// to div and mod
   763 
   764 MAKE-ALL (Poly/ML) ran perfectly.  It took 1:48 hours on albatross.
   765 
   766 **** New tar file 92.tar.z placed on /homes/lcp (376K) **** 
   767 
   768 Pure/NJ/commit: new dummy function
   769 FOLP/ex/ROOT: inserted commit call to avoid Poly/ML problems
   770 
   771 make-all: now builds FOLP also!
   772 
   773 3 June
   774 
   775 ZF/zf.thy,HOL/list.thy,HOL/set.thy: now constructions involving {_}, [_],
   776 <_,_> are formatted as {(_)}, [(_)], 
   777 
   778 MAKE-ALL (Poly/ML) ran perfectly.  It took 4:37 hours on muscovy (with FOLP).
   779 
   780 ZF/Makefile: removed obsolete target for .rules.ML
   781 
   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
   784 executing image.
   785 
   786 4 June
   787 
   788 Pure/logic/rewritec: now uses nets for greater speed.  Functor LogicFun now
   789 takes Net as argument.
   790 
   791 Pure/ROOT: now loads net before logic.
   792 
   793 MAKE-ALL (Poly/ML) failed in ZF and HOL.
   794 
   795 LK/lk.thy: changed constant "not" to "Not" (for consistency with FOL)
   796 
   797 7 June
   798 
   799 Pure/tactic/is_letdig: moved to library
   800 Pure/Syntax/lexicon/is_qld: deleted, was same as is_letdig
   801 
   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.
   804 
   805 HOL/set/UN1,INT1: new union/intersection operators.  Binders UN x.B(x),
   806 INT x.B(x).
   807 
   808 HOL/univ,llist: now use UN x.B(x) instead of Union(range(B))
   809 
   810 HOL/subset: added lattice properties for INT, UN (both forms)
   811 
   812 8 June
   813 
   814 MAKE-ALL (NJ 0.93) ran perfectly.  It took 4:45 hours on dunlin.
   815 
   816 **** New tar file 92.tar.z placed on /homes/lcp (384K) **** 
   817 
   818 14 June
   819 
   820 HOL/list.thy/List_rec_def: changed pred_sexp (a variable!) to pred_Sexp.
   821 Using def_wfrec hides such errors!!
   822 
   823 **** New tar file 92.tar.gz placed on /homes/lcp (384K) **** 
   824 
   825 ** NEW VERSION FROM MUNICH WITH ==-REWRITING **
   826 
   827 ** The following changes are Toby's **
   828 
   829 type.ML:
   830 
   831 Renamed mark_free to freeze_vars and thaw_tvars to thaw_vars.
   832 Added both functions to the signature.
   833 
   834 sign.ML:
   835 
   836 Added val subsig: sg * sg -> bool to signature.
   837 Added trueprop :: prop and mark_prop : prop => prop to pure_sg.
   838 
   839 Added
   840 
   841 val freeze_vars: term -> term
   842 val thaw_vars: term -> term
   843 val strip_all_imp: term * int -> term list * term * int
   844 
   845 Moved rewritec_bottom and rewritec_top to thm.ML.
   846 Only bottom-up rewriting supported any longer.
   847 
   848 thm.ML:
   849 
   850 Added
   851 
   852 (* internal form of conditional ==-rewrite rules *)
   853 type meta_simpset
   854 val add_mss: meta_simpset * thm list -> meta_simpset
   855 val empty_mss: meta_simpset
   856 val mk_mss: thm list -> meta_simpset
   857 
   858 val mark_prop_def: thm
   859 val truepropI: thm
   860 val trueprop_def: thm
   861 
   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)
   865                    -> Sign.cterm -> thm
   866 val trace_simp: bool ref
   867 
   868 Simplified concl_of: call to Logic.skip_flexpairs redundant.
   869 
   870 drule.ML:
   871 
   872 Added
   873 
   874 (* rewriting *)
   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
   878 
   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
   888 
   889 (*Moved here from tactic.ML:*)
   890 val asm_rl: thm
   891 val cut_rl: thm
   892 val revcut_rl: thm
   893 
   894 tactic.ML:
   895 
   896 Added
   897 
   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
   903 
   904 Moved to drule.ML:
   905 val asm_rl: thm
   906 val cut_rl: thm
   907 val revcut_rl: thm
   908 
   909 goals.ML:
   910 
   911 Changed prepare_proof to make sure that rewriting with empty list of
   912 meta-thms is identity.
   913 
   914 ** End of Toby's changes **
   915 
   916 16 June
   917 
   918 Pure/sign/typ_of,read_ctyp: new
   919 Pure/logic/dest_flexpair: now exported
   920 
   921 Pure/drule/flexpair_intr,flexpair_elim: new; fixes a bug in
   922 flexpair_abs_elim_list
   923 
   924 HOL/equalities/image_empty,image_insert: new
   925 HOL/ex/finite/Fin_imageI: new
   926 
   927 Installed Martin Coen's CCL as new object-logic
   928 
   929 17 June
   930 
   931 ** More changes from Munich (Markus Wenzel) **
   932 
   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
   938 
   939 HOL now exceeds poly's default heap size. Hence HOL/Makefile needs to
   940 specify -h 8000.
   941 
   942 HOL/univ/ntrunc_subsetD, etc: deleted the useless j<k assumption
   943 
   944 18 June
   945 
   946 MAKE-ALL (Poly/ML) ran perfectly.  It took 4:59 hours on dunlin (with CCL).
   947 
   948 Pure/sign/read_def_cterm: now prints the offending terms, as well as the
   949 types, when exception TYPE is raised.
   950 
   951 HOL/llist: some tidying
   952 
   953 23 June
   954 
   955 HOL/llist/Lconst_type: generalized from Lconst(M): LList({M})
   956 
   957 24 June
   958 
   959 MAKE-ALL (Poly/ML) ran perfectly.  It took 2:23 hours on albatross (with CCL)
   960 
   961 MAKE-ALL (NJ 0.93) failed in CCL due to use of "abstraction" as an
   962 identifier in CCL.ML
   963 
   964 **** New tar file 92.tar.gz placed on /homes/lcp (384K) **** (with CCL)
   965 
   966 CCL/ROOT: added ".ML" extension to use commands for NJ compatibility
   967 
   968 25 June
   969 
   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
   972 
   973 HOL/fun/rangeE,imageE: eta-expanded f to get variable name preservation
   974 
   975 HOL/llist/iterates_equality,lmap_lappend_distrib: tidied
   976 
   977 28 June
   978 
   979 HOL/set/UN1_I: made the Var and Bound variables agree ("x") to get variable
   980 name preservation 
   981 
   982 HOL/llist: co-induction rules applied with res_inst_tac to state the
   983 bisimulation directly
   984 
   985 2 July
   986 
   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.
   989 
   990 92/Makefile/$(BIN)/Pure: changed echo makefile= to echo database=
   991 
   992 **** New tar file 92.tar.gz placed on /homes/lcp (424K) **** (with CCL)
   993 
   994 
   995 ** NEW VERSION FROM MUNICH WITH ABSTRACT SYNTAX TREES & NEW PARSER **
   996 
   997 I have merged in the changes shown above since 24 June
   998 
   999 CHANGES LOG OF Markus Wenzel (MMW)
  1000 =======
  1001 
  1002 29-Jun-1993 MMW
  1003   *** Beta release of new syntax module ***
  1004   (should be 99% backwards compatible)
  1005 
  1006   Pure/Thy/ROOT.ML
  1007     added keywords for "translations" section
  1008 
  1009   Pure/Thy/syntax.ML
  1010     minor cleanup
  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, ...)
  1015 
  1016   Pure/Thy/read.ML
  1017     read_thy: added close_in
  1018     added file_exists (not perfect)
  1019     use_thy: now uses file_exists
  1020 
  1021   Pure/thm.ML
  1022     added syn_of: theory -> syntax
  1023 
  1024   Pure/Makefile
  1025     SYNTAX_FILES: added Syntax/ast.ML
  1026 
  1027   Pure/Syntax/pretty.ML
  1028     added str_of: T -> string
  1029 
  1030   Pure/Syntax/ast.ML
  1031     added this file
  1032 
  1033   Pure/Syntax/extension.ML
  1034   Pure/Syntax/parse_tree.ML
  1035   Pure/Syntax/printer.ML
  1036   Pure/Syntax/ROOT.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.
  1043 
  1044 
  1045 30-Jun-1993 MMW
  1046   New versions of HOL and Cube: use translation rules wherever possible;
  1047 
  1048   HOL/hol.thy
  1049     cleaned up
  1050     removed alt_tr', mk_bindopt_tr'
  1051     alternative binders now implemented via translation rules and mk_alt_ast_tr'
  1052 
  1053   HOL/set.thy
  1054     cleaned up
  1055     removed type "finset"
  1056     now uses category "args" for finite sets
  1057     junked "ML" section
  1058     added "translations" section
  1059 
  1060   HOL/list.thy
  1061     cleaned up
  1062     removed type "listenum"
  1063     now uses category "args" for lists
  1064     junked "ML" section
  1065     added "translations" section
  1066 
  1067   Cube/cube.thy
  1068     cleaned up
  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
  1073 
  1074 
  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?);
  1083 
  1084   Pure/NJ.ML
  1085     removed dummy install_pp
  1086     added make_pp, install_pp
  1087 
  1088   Pure/POLY.ML
  1089     removed dummy install_pp_nj
  1090     added make_pp
  1091 
  1092   Pure/ROOT.ML
  1093     removed install_pp_nj stuff
  1094 
  1095   Pure/drule.ML
  1096     added str_of_sg, str_of_theory, str_of_thm
  1097 
  1098   Pure/install_pp.ML
  1099     added this file
  1100 
  1101   Pure/sign.ML
  1102     added str_of_term, str_of_typ, str_of_cterm, str_of_ctyp
  1103 
  1104   Pure/goals.ML
  1105     added str_of_term, str_of_typ
  1106 
  1107   CTT/ROOT.ML
  1108   Cube/ROOT.ML
  1109   FOL/ROOT.ML
  1110   FOLP/ROOT.ML
  1111   HOL/ROOT.ML
  1112   LK/ROOT.ML
  1113     replaced install_pp stuff by 'use "../Pure/install_pp.ML"'
  1114 
  1115 
  1116 01-Jul-1993 MMW
  1117   Misc small fixes
  1118 
  1119   CCL/ROOT.ML
  1120   HOL/ROOT.ML
  1121     added ".ML" suffix to some filenames
  1122 
  1123   HOL/ex/unsolved.ML
  1124     replaced HOL_Rule.thy by HOL.thy
  1125 
  1126   Pure/NJ.ML
  1127     quit was incorrectly int -> unit
  1128 
  1129 END MMW CHANGES
  1130 
  1131 Pure/Syntax/sextension/eta_contract: now initially false 
  1132 
  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
  1136 
  1137 Pure/goals/prove_goalw: now prints some of the information from print_exn
  1138 
  1139 9 July
  1140 
  1141 MAKE-ALL (Poly/ML) ran perfectly.  It took 2:26 hours on albatross.
  1142 
  1143 **** New tar file 93.tar.gz placed on /homes/lcp (480K) **** 
  1144 
  1145 12 July
  1146 
  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.
  1149 
  1150 22 July
  1151 
  1152 ZF/zf.thy: new version from Marcus Wenzel
  1153 
  1154 ZF: ** installation of inductive definitions **
  1155 
  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
  1158 pair.ML  ex/integ.ML
  1159 
  1160 changing the argument order of "case" and adding "Part": sum.thy sum.ML
  1161 
  1162 ZF/zf.ML/rev_subsetD,rev_bspec: new
  1163 
  1164 ZF/mono: new rules for implication
  1165 ZF/mono/Collect_mono: now for use with implication rules
  1166 
  1167 ZF/zf.ML/ballE': renamed rev_ballE
  1168 
  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.
  1172 
  1173 ZF/extend_ind.ML, datatype.ML: new files
  1174 ZF/fin.ML: moved from ex/finite.ML
  1175 
  1176 23 July
  1177 
  1178 ZF/ex/sexp: deleted this example -- it seems hardly worth the trouble of
  1179 porting.
  1180 
  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
  1183 
  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
  1186 
  1187 ZF/sum/InlI,InrI: renamed from sum_InlI, sum_InlI
  1188 
  1189 26 July
  1190 
  1191 ZF/univ/rank_ss: new, for proving recursion equations
  1192 
  1193 ZF/domrange/image_iff,image_singleton_iff,vimage_iff,vimage_singleton_iff,
  1194 field_of_prod:new
  1195 
  1196 ZF/domrange/field_subset: modified
  1197 
  1198 ZF/list/list_cases: no longer proved by induction!
  1199 ZF/wf/wf_trancl: simplified proof
  1200 
  1201 ZF/equalities: new laws for field
  1202 
  1203 29 July
  1204 
  1205 ZF/trancl/trancl_induct: new
  1206 ZF/trancl/rtrancl_induct,trancl_induct: now with more type information
  1207 
  1208 ** More changes from Munich (Markus Wenzel) **
  1209 
  1210 Update of new syntax module (aka macro system): mostly internal cleanup and
  1211 polishing;
  1212 
  1213   Pure/Syntax/*
  1214     added Ast.stat_norm
  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'
  1221 
  1222   Pure/sign.ML: removed declaration of "==>" (now in Syntax.pure_sext)
  1223 
  1224 Changes to object logics: minor cleanups and replacement of most remaining ML
  1225 translations by rewrite rules (see also file "Translations");
  1226 
  1227   ZF/zf.thy
  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
  1232 
  1233   Cube/cube.thy
  1234     removed necontext
  1235     replaced fun_tr/tr' by ndependent_tr/dependent_tr'
  1236 
  1237   CTT/ctt.thy
  1238     added translations rules for PROD and SUM
  1239     removed dependent_tr
  1240     removed definitions of ndependent_tr, dependent_tr'
  1241 
  1242   HOL/set.thy: replaced id by idt
  1243 
  1244   CCL/ROOT.ML: Logtic -> Logic
  1245 
  1246   CCL/set.thy
  1247     added "translations" section
  1248     removed "ML" section
  1249     replaced id by idt
  1250 
  1251   CCL/types.thy
  1252     added "translations" section
  1253     removed definitions of ndependent_tr, dependent_tr'
  1254     replaced id by idt
  1255 
  1256 Yet another improvement of toplevel pretty printers: output now breakable;
  1257 
  1258   Pure/NJ.ML Pure/POLY.ML improved make_pp
  1259 
  1260   Pure/install_pp.ML: replaced str_of_* by pprint_*
  1261 
  1262   Pure/drule.ML: replaced str_of_{sg,theory,thm} by pprint_*
  1263 
  1264   Pure/sign.ML: replaced str_of_{term,typ,cterm,ctyp} by pprint_*
  1265 
  1266   Pure/goals.ML: fixed and replaced str_of_{term,typ} by pprint_*
  1267 
  1268   Pure/Syntax/pretty.ML: added pprint, quote
  1269 
  1270 Minor changes and additions;
  1271 
  1272   Pure/sign.ML: renamed stamp "PURE" to "Pure"
  1273 
  1274   Pure/library.ML
  1275     added quote: string -> string
  1276     added to_lower: string -> bool
  1277 
  1278   Pure/NJ.ML,POLY.ML: added file_info of Carsten Clasohm
  1279 
  1280 30 July
  1281 
  1282 MAKE-ALL (Poly/ML) ran perfectly.
  1283 
  1284 Pure/goals/print_sign_exn: new, takes most code from print_exn
  1285 Pure/goals/prove_goalw: displays exceptions using print_sign_exn
  1286 
  1287 Pure/drule/print_sg: now calls pretty_sg to agree with pprint_sg
  1288 
  1289 Pure/library,...: replaced front/nth_tail by take/drop.
  1290 
  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
  1293 
  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
  1297 
  1298 Pure/term/subst_free: new
  1299 
  1300 Pure/tactic/is_fact: newly exported
  1301 
  1302 Provers/simp/mk_congs: uses filter_out is_fact to delete trivial cong rules
  1303 
  1304 Pure/tactic/rename_last_tac: now uses Syntax.is_identifier instead of
  1305 forall is_letdig
  1306 
  1307 **** New tar file 93.tar.gz placed on /homes/lcp (448K) **** 
  1308 
  1309 2 August
  1310 
  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.
  1313 
  1314 Pure/drule/triv_forall_equality: new
  1315 Pure/tactic/prune_params_tac: new
  1316 
  1317 Provers/hypsubst/bound_hyp_subst_tac: new, safer than hyp_subst_tac
  1318 
  1319 3 August
  1320 
  1321 Pure/tactic/rule_by_tactic: new
  1322 
  1323 ZF/perm/compEpair: now proved via rule_by_tactic
  1324 
  1325 ZF/extend_ind/cases,mk_cases: new
  1326 ZF/datatype/mk_free: new
  1327 ZF/list: now calls List.mk_cases
  1328 
  1329 4 August
  1330 
  1331 Provers/slow_tac,slow_best_tac: new
  1332 
  1333 5 August
  1334 
  1335 MAKE-ALL (Poly/ML) failed in ZF
  1336 
  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
  1340 
  1341 6 August
  1342 
  1343 Pure/goals/prepare_proof: after "Additional hypotheses", now actually
  1344 prints them!
  1345 
  1346 ZF/ordinal/Transset_Union_family, Transset_Inter_family: renamed from
  1347 Transset_Union, Transset_Inter
  1348 
  1349 ZF/ordinal/Transset_Union: new 
  1350 ZF/univ/pair_in_univ: renamed Pair_in_univ
  1351 
  1352 ZF/mono/product_mono: generalized to Sigma_mono; changed uses in trancl, univ
  1353 
  1354 ZF/lfp/lfp_Tarski,def_lfp_Tarski: renamed from Tarski,def_Tarski; changed
  1355 uses in extend_ind.ML, nat.ML, trancl.ML.
  1356 
  1357 ZF/ex/misc: Schroeder-Bernstein Theorem moved here from lfp.ML
  1358 
  1359 ZF/fixedpt.thy,.ML: renamed from lfp.thy,.ML, and gfp added
  1360 
  1361 9 August
  1362 
  1363 ZF/zf.thy/ndependent_tr,dependent_tr': deleted, since they are now on
  1364 Syntax/sextension. 
  1365 
  1366 11 August
  1367 
  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
  1371 
  1372 Pure/type.ML: deleted (inefficient) transitive_closure