edits.txt
changeset 13893 19849d258890
parent 13892 4ac9d55573da
child 13894 8018173a7979
equal deleted inserted replaced
13892:4ac9d55573da 13893:19849d258890
     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