edits.txt
author paulson
Tue Aug 03 13:04:50 1999 +0200 (1999-08-03)
changeset 7157 d49318f6c11a
parent 0 a5a9c433f639
permissions -rw-r--r--
SVC
clasohm@0
     1
EDITS TO THE ISABELLE SYSTEM FOR 1993
clasohm@0
     2
clasohm@0
     3
11 January 
clasohm@0
     4
clasohm@0
     5
*/README: Eliminated references to Makefile.NJ, which no longer exists.
clasohm@0
     6
clasohm@0
     7
**** New tar file placed on /homes/lcp (464K) **** 
clasohm@0
     8
clasohm@0
     9
14 January
clasohm@0
    10
clasohm@0
    11
Provers/simp/pr_goal_lhs: now distinct from pr_goal_concl so that tracing
clasohm@0
    12
prints conditions correctly.
clasohm@0
    13
clasohm@0
    14
{CTT/arith,HOL/ex/arith/ZF/arith}/add_mult_distrib: renamed from
clasohm@0
    15
add_mult_dist, to agree with the other _distrib rules
clasohm@0
    16
clasohm@0
    17
20 January
clasohm@0
    18
clasohm@0
    19
Pure/Syntax/type_ext.ML: "I have fixed a few anomalies in the pretty
clasohm@0
    20
printing annotations for types.  Only the layout has changed." -- Toby
clasohm@0
    21
clasohm@0
    22
21 January
clasohm@0
    23
clasohm@0
    24
{CTT/arith,HOL/ex/arith/ZF/arith}/add_inverse_diff: renamed to add_diff_inverse
clasohm@0
    25
clasohm@0
    26
22 January
clasohm@0
    27
clasohm@0
    28
ZF/ex/equiv: new theory of equivalence classes
clasohm@0
    29
ZF/ex/integ: new theory of integers
clasohm@0
    30
HOL/set.thy: added indentation of 3 to all binding operators
clasohm@0
    31
clasohm@0
    32
ZF/bool/boolI0,boolI1: renamed as bool_0I, bool_1I
clasohm@0
    33
clasohm@0
    34
25 January
clasohm@0
    35
clasohm@0
    36
MAKE-ALL (NJ 0.75) ran perfectly.  It took 3:19 hours!?
clasohm@0
    37
clasohm@0
    38
ZF/bool/not,and,or,xor: new
clasohm@0
    39
clasohm@0
    40
27 January
clasohm@0
    41
clasohm@0
    42
ZF/ex/bin: new theory of binary integer arithmetic
clasohm@0
    43
clasohm@0
    44
27 January
clasohm@0
    45
clasohm@0
    46
MAKE-ALL (Poly/ML) ran perfectly.  It took 6:33 hours???
clasohm@0
    47
(ZF took almost 5 hours!)
clasohm@0
    48
clasohm@0
    49
**** New tar file placed on /homes/lcp (472K) **** 
clasohm@0
    50
clasohm@0
    51
HOL/set/UN_cong,INT_cong: new
clasohm@0
    52
HOL/subset/mem_rews,set_congs,set_ss: new
clasohm@0
    53
HOL/simpdata/o_apply: new; added to HOL_ss
clasohm@0
    54
clasohm@0
    55
29 January
clasohm@0
    56
clasohm@0
    57
Pure/Thy/syntax/mk_structure: the dummy theory created by type infixes is
clasohm@0
    58
now called name^"(type infix)" instead of "", avoid triggering a spurious
clasohm@0
    59
error "Attempt to merge different versions of theory: " in
clasohm@0
    60
Pure/sign/merge_stamps
clasohm@0
    61
clasohm@0
    62
2 February
clasohm@0
    63
clasohm@0
    64
MAKE-ALL (Poly/ML) ran perfectly.  It took 2:48 hours.  Runs in 1992 took
clasohm@0
    65
under 2:20 hours, but the new files in ZF/ex take time: nearly 23 minutes
clasohm@0
    66
according to make10836.log.
clasohm@0
    67
clasohm@0
    68
Pure/Thy/scan/comment: renamed from komt
clasohm@0
    69
Pure/Thy/scan/numeric: renamed from zahl
clasohm@0
    70
clasohm@0
    71
Pure/Syntax/syntax,lexicon,type_ext,extension,sextension: modified by
clasohm@0
    72
Tobias to change ID, TVAR, ... to lower case.
clasohm@0
    73
clasohm@0
    74
Cube/cube.thy,HOL/hol.thy,HOL/set.thy,CTT/ctt.thy,LK/lk.thy,ZF/zf.thy: now
clasohm@0
    75
with ID, ... in lower case and other tidying
clasohm@0
    76
clasohm@0
    77
3 February
clasohm@0
    78
clasohm@0
    79
MAKE-ALL (Poly/ML) ran perfectly.  It took 2:50 hours.
clasohm@0
    80
clasohm@0
    81
4 February
clasohm@0
    82
clasohm@0
    83
HOL/nat/nat_ss: now includes the rule Suc_less_eq: (Suc(m) < Suc(n)) = (m<n)
clasohm@0
    84
and the nat_case rules and congruence rules
clasohm@0
    85
clasohm@0
    86
HOL/sum/sumE: now has the "strong" form with equality assumptions.  WAS
clasohm@0
    87
    val prems = goalw Sum.thy [Inl_def,Inr_def]
clasohm@0
    88
	"[| !!x::'a. P(Inl(x));  !!y::'b. P(Inr(y)) \
clasohm@0
    89
    \    |] ==> P(s)";
clasohm@0
    90
    by (res_inst_tac [("t","s")] (Rep_Sum_inverse RS subst) 1);
clasohm@0
    91
    by (rtac (rewrite_rule [Sum_def] Rep_Sum RS CollectE) 1);
clasohm@0
    92
    by (REPEAT (eresolve_tac [disjE,exE,ssubst] 1 ORELSE resolve_tac prems 1));
clasohm@0
    93
    val sumE = result();
clasohm@0
    94
clasohm@0
    95
8 February
clasohm@0
    96
clasohm@0
    97
Changes from Tobias:
clasohm@0
    98
Pure/Thy/parse: now list_of admits the empty phrase, while listof_1 does not
clasohm@0
    99
Pure/Thy/syntax: uses new list_of, list_of1
clasohm@0
   100
clasohm@0
   101
9 February
clasohm@0
   102
clasohm@0
   103
HOL/ex/arith: moved to main HOL directory
clasohm@0
   104
HOL/prod: now define the type "unit" and constant "(): unit"
clasohm@0
   105
clasohm@0
   106
11 February
clasohm@0
   107
clasohm@0
   108
HOL/arith: eliminated redefinitions of nat_ss and arith_ss
clasohm@0
   109
clasohm@0
   110
12 February
clasohm@0
   111
clasohm@0
   112
MAKE-ALL (Poly/ML) ran perfectly.  It took 2:50 hours.
clasohm@0
   113
clasohm@0
   114
Pure/Thy/scan/string: now correctly recognizes ML-style strings.
clasohm@0
   115
clasohm@0
   116
15 February
clasohm@0
   117
clasohm@0
   118
MAKE-ALL (NJ 0.75) ran perfectly.  It took 1:37 hours (on albatross)
clasohm@0
   119
MAKE-ALL (NJ 0.75) ran perfectly.  It took 2:42 hours (on dunlin)
clasohm@0
   120
MAKE-ALL (Poly/ML) ran perfectly.  It took 2:53 hours (on dunlin)
clasohm@0
   121
clasohm@0
   122
**** New tar file placed on /homes/lcp (480K) **** 
clasohm@0
   123
clasohm@0
   124
18 February
clasohm@0
   125
clasohm@0
   126
Pure/Syntax/earley0A/compile_xgram: Tobias deleted the third argument, as
clasohm@0
   127
it was unused.
clasohm@0
   128
clasohm@0
   129
Pure/Syntax/earley0A: modified accordingly.
clasohm@0
   130
clasohm@0
   131
19 February
clasohm@0
   132
clasohm@0
   133
MAKE-ALL (NJ 0.75) ran perfectly.  It took 3:37 hours 
clasohm@0
   134
MAKE-ALL (Poly/ML) ran perfectly.  It took 2:52 hours
clasohm@0
   135
clasohm@0
   136
**** New tar file placed on /homes/lcp (480K) **** 
clasohm@0
   137
clasohm@0
   138
20 February
clasohm@0
   139
clasohm@0
   140
MAKE-ALL (NJ 0.93) ran perfectly.  It took 3:30 hours 
clasohm@0
   141
clasohm@0
   142
10 March
clasohm@0
   143
clasohm@0
   144
HOL/fun/image_eqI: fixed bad pattern
clasohm@0
   145
clasohm@0
   146
11 March
clasohm@0
   147
clasohm@0
   148
MAKE-ALL (Poly/ML) failed in HOL!
clasohm@0
   149
clasohm@0
   150
HOL/fun: moved "mono" proofs to HOL/subset, since they rely on subset laws
clasohm@0
   151
of Int and Un.
clasohm@0
   152
clasohm@0
   153
12 March
clasohm@0
   154
clasohm@0
   155
ZF/ex/misc: new example from Bledsoe
clasohm@0
   156
clasohm@0
   157
15 March
clasohm@0
   158
clasohm@0
   159
ZF/perm: two new theorems inspired by Pastre
clasohm@0
   160
clasohm@0
   161
16 March
clasohm@0
   162
clasohm@0
   163
Weakened congruence rules for HOL: speeds simplification considerably by
clasohm@0
   164
NOT simplifying the body of a conditional or eliminator.
clasohm@0
   165
clasohm@0
   166
HOL/simpdata/mk_weak_congs: new, to make weakened congruence rules
clasohm@0
   167
clasohm@0
   168
HOL/simpdata/congs: renamed HOL_congs and weakened the "if" rule
clasohm@0
   169
clasohm@0
   170
HOL/simpdata/HOL_congs: now contains polymorphic rules for the overloaded
clasohm@0
   171
operators < and <=
clasohm@0
   172
clasohm@0
   173
HOL/prod: weakened the congruence rule for split
clasohm@0
   174
HOL/sum: weakened the congruence rule for case
clasohm@0
   175
HOL/nat: weakened the congruence rule for nat_case and nat_rec
clasohm@0
   176
HOL/list: weakened the congruence rule for List_rec and list_rec
clasohm@0
   177
clasohm@0
   178
HOL & test rebuilt perfectly
clasohm@0
   179
clasohm@0
   180
Pure/goals/prepare_proof/mkresult: fixed bug in signature check.  Now
clasohm@0
   181
compares the FINAL signature with that from the original theory.
clasohm@0
   182
clasohm@0
   183
Pure/goals/prepare_proof: ensures that [prove_]goalw checks that the
clasohm@0
   184
definitions do not update the proof state.
clasohm@0
   185
clasohm@0
   186
17 March
clasohm@0
   187
clasohm@0
   188
MAKE-ALL (Poly/ML) ran perfectly.
clasohm@0
   189
clasohm@0
   190
18 March
clasohm@0
   191
clasohm@0
   192
MAKE-ALL (Poly/ML) failed in HOL/ex/Substitutions
clasohm@0
   193
clasohm@0
   194
HOL/ex/Subst/setplus: changed Set.thy to Setplus.thy where
clasohm@0
   195
necessary
clasohm@0
   196
clasohm@0
   197
ZF/perm: proved some rules about inj and surj
clasohm@0
   198
clasohm@0
   199
ZF/ex/misc: did some of Pastre's examples
clasohm@0
   200
clasohm@0
   201
Pure/library/gen_ins,gen_union: new
clasohm@0
   202
clasohm@0
   203
HOL/ex/Subst/subst: renamed rangeE to srangeE
clasohm@0
   204
clasohm@0
   205
18 March
clasohm@0
   206
clasohm@0
   207
MAKE-ALL (Poly/ML) failed in HOL/ex/term due to renaming of list_ss in
clasohm@0
   208
ex/Subst/alist
clasohm@0
   209
clasohm@0
   210
HOL/list/list_congs: new; re-organized simpsets a bit
clasohm@0
   211
clasohm@0
   212
Pure/goals/sign_error: new
clasohm@0
   213
clasohm@0
   214
Pure/goals/prepare_proof,by_com: now print the list of new theories when
clasohm@0
   215
the signature of the proof state changes 
clasohm@0
   216
clasohm@0
   217
HOL/prod,sexp: renamed fst, snd to fst_conv, snd_conv to avoid over-writing
clasohm@0
   218
the library functions fst, snd
clasohm@0
   219
clasohm@0
   220
HOL/fun/image_compose: new
clasohm@0
   221
clasohm@0
   222
21 March
clasohm@0
   223
clasohm@0
   224
MAKE-ALL (NJ 0.93) ran perfectly.  It took 3:50 hours 
clasohm@0
   225
MAKE-ALL (Poly/ML) ran perfectly.  It took 3:21 hours
clasohm@0
   226
Much slower now (about 30 minutes!) because of HOL/ex/Subst
clasohm@0
   227
clasohm@0
   228
**** New tar file placed on /homes/lcp (504K) **** 
clasohm@0
   229
clasohm@0
   230
ZF/pair,simpdata: renamed fst, snd to fst_conv, snd_conv to avoid over-writing
clasohm@0
   231
the library functions fst, snd
clasohm@0
   232
clasohm@0
   233
HOL/prod/prod_fun_imageI,E: new
clasohm@0
   234
clasohm@0
   235
HOL/ex/Subst/Unify: renamed to Unifier to avoid clobbering structure Unify
clasohm@0
   236
of Pure
clasohm@0
   237
clasohm@0
   238
24 March
clasohm@0
   239
clasohm@0
   240
HOL/trancl/comp_subset_Sigma: new
clasohm@0
   241
HOL/wf/wfI: new
clasohm@0
   242
clasohm@0
   243
HOL/Subst: moved from HOL/ex/Subst to shorten pathnames
clasohm@0
   244
HOL/Makefile: target 'test' now loads Subst/ROOT separately
clasohm@0
   245
clasohm@0
   246
*** Installation of gfp, coinduction, ... to HOL ***
clasohm@0
   247
clasohm@0
   248
HOL/gfp,llist: new
clasohm@0
   249
HOL/univ,sexp,list: replaced with new version
clasohm@0
   250
clasohm@0
   251
Sexp is now the set of all well-founded trees, each of type 'a node set.
clasohm@0
   252
There is no longer a type 'sexp'.  Initial algebras require more explicit
clasohm@0
   253
type checking than before.  Defining a type 'sexp' would eliminate this,
clasohm@0
   254
but would also require a whole new set of primitives, similar to those
clasohm@0
   255
defined in univ.thy but restricted to well-founded trees.
clasohm@0
   256
clasohm@0
   257
25 March
clasohm@0
   258
clasohm@0
   259
Pure/thm: renamed 'bires' to 'eres' in many places (not exported) --
clasohm@0
   260
biresolution now refers to resolution with (flag,rule) pairs.
clasohm@0
   261
clasohm@0
   262
Pure/thm/bicompose_aux: SOUNDNESS BUG concerning variable renaming.  A Var in
clasohm@0
   263
a premise was getting renamed when its occurrence in the flexflex pairs was
clasohm@0
   264
not.  Martin Coen supplied the following proof of True=False in HOL:
clasohm@0
   265
clasohm@0
   266
    val [prem] = goal Set.thy "EX a:{c}.p=a ==> p=c";
clasohm@0
   267
    br (prem RS bexE) 1; be ssubst 1; be singletonD 1;
clasohm@0
   268
    val l1 = result();
clasohm@0
   269
clasohm@0
   270
    val rls = [refl] RL [bexI] RL [l1];
clasohm@0
   271
clasohm@0
   272
    goal Set.thy "True = False";
clasohm@0
   273
    brs rls 1; br singletonI 1;
clasohm@0
   274
    result();
clasohm@0
   275
clasohm@0
   276
Marcus Moore noted that the error only occurred with
clasohm@0
   277
Logic.auto_rename:=false.  Elements of the fix:
clasohm@0
   278
clasohm@0
   279
1.  rename_bvs, rename_bvars and bicompose_aux/newAs take tpairs (the
clasohm@0
   280
existing flex-flex pairs) as an extra argument.  rename_bvs preserves all
clasohm@0
   281
Vars in tpairs.
clasohm@0
   282
clasohm@0
   283
2.  bicompose_aux/tryasms and res now unpack the "cell" and supply its tpairs
clasohm@0
   284
to newAs.
clasohm@0
   285
clasohm@0
   286
HOL/lfp,gfp,ex/set: renamed Tarski to lfp_Tarski
clasohm@0
   287
clasohm@0
   288
HOL/lfp,list,llist,nat,sexp,trancl,Subst/uterm,ex/simult,ex/term: renamed
clasohm@0
   289
def_Tarski to def_lfp_Tarski 
clasohm@0
   290
clasohm@0
   291
26 March
clasohm@0
   292
clasohm@0
   293
MAKE-ALL (NJ 0.93) ran perfectly.  It took 4:25 hours!
clasohm@0
   294
MAKE-ALL (Poly/ML) ran perfectly.  It took 3:54 hours! (jobs overlapped)
clasohm@0
   295
clasohm@0
   296
Pure/Thy/scan/is_digit,is_letter: deleted.  They are already in
clasohm@0
   297
Pure/library, and these versions used non-Standard string comparisons!
clasohm@0
   298
clasohm@0
   299
Repairing a fault reported by David Aspinall:
clasohm@0
   300
  show_types := true;  read "a";  (* followed by  'prin it' for NJ *)
clasohm@0
   301
Raises exception  LIST "hd".   Also has the side effect of leaving
clasohm@0
   302
show_types set at false. 
clasohm@0
   303
clasohm@0
   304
Pure/goals/read: no longer creates a null TVar
clasohm@0
   305
Pure/Syntax/lexicon/string_of_vname: now handles null names
clasohm@0
   306
Pure/Syntax/printer/string_of_typ: tidied
clasohm@0
   307
clasohm@0
   308
/usr/groups/theory/isabelle/92/Pure/thm: replaced by new version to fix bug
clasohm@0
   309
MAKE-ALL on this directory ran perfectly
clasohm@0
   310
/usr/groups/theory/ml-aftp/Isabelle92.tar.Z: replaced by new version
clasohm@0
   311
clasohm@0
   312
29 March
clasohm@0
   313
clasohm@0
   314
MAKE-ALL (NJ 0.93) ran perfectly.  It took 4:14 hours!
clasohm@0
   315
MAKE-ALL (Poly/ML) ran perfectly.  It took 3:43 hours!
clasohm@0
   316
clasohm@0
   317
**** New tar file placed on /homes/lcp (518K) **** 
clasohm@0
   318
clasohm@0
   319
30 March
clasohm@0
   320
clasohm@0
   321
ZF/univ/cons_in_Vfrom: deleted "[| a: Vfrom(A,i);  b<=Vfrom(A,i) |] ==>
clasohm@0
   322
cons(a,b) : Vfrom(A,succ(i))" since it was useless.
clasohm@0
   323
clasohm@0
   324
8 April
clasohm@0
   325
clasohm@0
   326
MAKE-ALL (Poly/ML) ran perfectly.  It took 3:49 hours!
clasohm@0
   327
clasohm@0
   328
**** New tar file placed on /homes/lcp (520K) **** 
clasohm@0
   329
clasohm@0
   330
**** Updates for pattern unification (Tobias Nipkow) ****
clasohm@0
   331
clasohm@0
   332
Pure/pattern.ML: new, pattern unification
clasohm@0
   333
clasohm@0
   334
Pure/Makefile and ROOT.ML: included pattern.ML
clasohm@0
   335
clasohm@0
   336
Pure/library.ML: added predicate downto0
clasohm@0
   337
clasohm@0
   338
Pure/unify.ML: call pattern unification first. Removed call to could_unify.
clasohm@0
   339
clasohm@0
   340
FOL/Makefile/FILES: now mentions ifol.ML (previously repeated fol.ML instead)
clasohm@0
   341
clasohm@0
   342
**** Installation of Martin Coen's FOLP (FOL + proof objects) ****
clasohm@0
   343
clasohm@0
   344
renamed PFOL, PIFOL to FOLP, IFOLP, etc.
clasohm@0
   345
clasohm@0
   346
9 April
clasohm@0
   347
clasohm@0
   348
MAKE-ALL (NJ 0.93) ran perfectly.  It took 4:05 hours!
clasohm@0
   349
MAKE-ALL (Poly/ML) ran perfectly.  It took 3:31 hours!
clasohm@0
   350
clasohm@0
   351
**** New tar file placed on /homes/lcp (576K) **** 
clasohm@0
   352
clasohm@0
   353
**** Installation of Discrimination Nets ****
clasohm@0
   354
clasohm@0
   355
*Affected files (those mentioning Stringtree, compat_thms or rtr_resolve_tac)
clasohm@0
   356
Pure/ROOT.ML,goals.ML,stringtree.ML,tactic.ML
clasohm@0
   357
Provers/simp.ML
clasohm@0
   358
HOL/ex/meson.ML
clasohm@0
   359
clasohm@0
   360
*Affected files (those mentioning compat_resolve_tac)
clasohm@0
   361
Pure/tactic.ML
clasohm@0
   362
Provers/typedsimp.ML
clasohm@0
   363
CTT/ctt.ML
clasohm@0
   364
clasohm@0
   365
Pure/stringtree: saved on Isabelle/old
clasohm@0
   366
Pure/net: new
clasohm@0
   367
Pure/Makefile/FILES: now mentions net.ML, not stringtree.ML
clasohm@0
   368
Pure/ROOT: now mentions net.ML, not stringtree.ML
clasohm@0
   369
clasohm@0
   370
Pure/goals/compat_goal: DELETED
clasohm@0
   371
clasohm@0
   372
Pure/tactic/compat_thms,rtr_resolve_tac,compat_resolve_tac,insert_thm,
clasohm@0
   373
delete_thm,head_string: DELETED
clasohm@0
   374
clasohm@0
   375
Pure/tactic/biresolve_from_nets_tac, bimatch_from_nets_tac,
clasohm@0
   376
net_biresolve_tac, net_bimatch_tac, resolve_from_net_tac, match_from_net_tac,
clasohm@0
   377
net_resolve_tac, net_match_tac: NEW
clasohm@0
   378
clasohm@0
   379
Pure/tactic/filt_resolve_tac: new implementation using nets!
clasohm@0
   380
clasohm@0
   381
Provers/simp: replaced by new version
clasohm@0
   382
clasohm@0
   383
Provers/typedsimp: changed compat_resolve_tac to filt_resolve_tac and
clasohm@0
   384
updated comments
clasohm@0
   385
clasohm@0
   386
CTT/ctt.ML: changed compat_resolve_tac to filt_resolve_tac 
clasohm@0
   387
ZF/simpdata/typechk_step_tac: changed compat_resolve_tac to filt_resolve_tac
clasohm@0
   388
clasohm@0
   389
CTT tested
clasohm@0
   390
clasohm@0
   391
HOL/ex/meson/ins_term,has_reps: replaced Stringtree by Net
clasohm@0
   392
clasohm@0
   393
FOL tested
clasohm@0
   394
clasohm@0
   395
Provers/simp/cong_const: new, replaces head_string call in cong_consts
clasohm@0
   396
Provers/simp: renamed variables: atomic to at and cong_consts to ccs
clasohm@0
   397
clasohm@0
   398
ZF/ex/bin/integ_of_bin_type: proof required reordering of rules --
clasohm@0
   399
typechk_tac now respects this ordering!
clasohm@0
   400
clasohm@0
   401
ZF tested
clasohm@0
   402
clasohm@0
   403
DOCUMENTATION
clasohm@0
   404
clasohm@0
   405
Logics/CTT: Removed mention of compat_resolve_tac 
clasohm@0
   406
Ref/goals: deleted compat_goal's entry
clasohm@0
   407
clasohm@0
   408
Provers/hypsubst/lasthyp_subst_tac: deleted
clasohm@0
   409
clasohm@0
   410
FOLP/ROOT/dest_eq: corrected; now hyp_subst_tac works!
clasohm@0
   411
clasohm@0
   412
12 April
clasohm@0
   413
clasohm@0
   414
MAKE-ALL (NJ 0.93) ran perfectly.  It took 4:03 hours!
clasohm@0
   415
MAKE-ALL (Poly/ML) ran perfectly.  It took 3:28 hours!
clasohm@0
   416
clasohm@0
   417
FOLP/{int-prover,classical}/safe_step_tac: uses eq_assume_tac, not assume_tac
clasohm@0
   418
FOLP/{int-prover,classical}/inst_step_tac: restored, calls assume and mp_tac
clasohm@0
   419
FOLP/{int-prover,classical}/step_tac: calls inst_step_tac 
clasohm@0
   420
clasohm@0
   421
{FOL,FOLP}/int-prover/safe_brls: removed (asm_rl,true) since assume_tac is
clasohm@0
   422
used explicitly!!
clasohm@0
   423
clasohm@0
   424
FOLP/ifolp/uniq_assume_tac: new, since eq_assume_tac is almost useless
clasohm@0
   425
clasohm@0
   426
FOLP/{int-prover,classical}/uniq_mp_tac: replace eq_mp_tac and call
clasohm@0
   427
uniq_assume_tac
clasohm@0
   428
clasohm@0
   429
Provers/classical: REPLACED BY 'NET' VERSION!
clasohm@0
   430
clasohm@0
   431
13 April
clasohm@0
   432
clasohm@0
   433
MAKE-ALL (Poly/ML) failed in ZF and ran out of quota for Cube.
clasohm@0
   434
clasohm@0
   435
Unification bug (nothing to do with pattern unification)
clasohm@0
   436
Cleaning of flex-flex pairs attempts to remove all occurrences of bound
clasohm@0
   437
variables not common to both sides.  Arguments containing "banned" bound
clasohm@0
   438
variables are deleted -- but this should ONLY be done if the occurrence is
clasohm@0
   439
rigid!
clasohm@0
   440
clasohm@0
   441
unify/CHANGE_FAIL: new, for flexible occurrence of bound variable
clasohm@0
   442
unify/change_bnos: now takes "flex" as argument, indicating path status
clasohm@0
   443
clasohm@0
   444
14 April
clasohm@0
   445
clasohm@0
   446
MAKE-ALL (Poly/ML) failed in HOL (ASM_SIMP_TAC redefined!) and LK
clasohm@0
   447
clasohm@0
   448
LK/ex/hard-quant/37: added "by flexflex_tac" to compensate for flexflex
clasohm@0
   449
changes
clasohm@0
   450
clasohm@0
   451
Pure/goals/gethyps: now calls METAHYPS directly
clasohm@0
   452
clasohm@0
   453
rm-logfiles: no longer mentions directories.  WAS
clasohm@0
   454
    rm log {Pure,FOL,ZF,LCF,CTT,LK,Modal,HOL,Cube}/make*.log
clasohm@0
   455
    rm {FOL,ZF,LCF,CTT,LK,Modal,HOL,Cube}/test
clasohm@0
   456
    rm {FOL,ZF,LCF,CTT,LK,Modal,HOL,Cube}/.*.thy.ML
clasohm@0
   457
    rm {FOL,ZF,HOL}/ex/.*.thy.ML
clasohm@0
   458
clasohm@0
   459
MAKE-ALL (Poly/ML) ran perfectly.  It took 2:39 hours! (albatross)
clasohm@0
   460
clasohm@0
   461
New version of simp on Isabelle/new -- instantiates unknowns provided only
clasohm@0
   462
one rule may do so [SINCE REJECTED DUE TO UNPREDICTABLE BEHAVIOR]
clasohm@0
   463
clasohm@0
   464
works with FOLP/ex/nat, but in general could fail in the event of
clasohm@0
   465
overlapping rewrite rules, since FOLP always instantiates unknowns during
clasohm@0
   466
rewriting.
clasohm@0
   467
clasohm@0
   468
ZF: tested with new version
clasohm@0
   469
clasohm@0
   470
HOL: tested with new version, appeared to loop in llist/Lmap_ident
clasohm@0
   471
clasohm@0
   472
**** NEW VERSION OF ASM_SIMP_TAC, WITH METAHYPS ****
clasohm@0
   473
clasohm@0
   474
ZF: failed in perm/comp_mem_injD1: the rule anti_refl_rew is too ambiguous!
clasohm@0
   475
ZF/wfrec: all uses of wf_ss' require
clasohm@0
   476
by (METAHYPS (fn hyps => cut_facts_tac hyps 1 THEN
clasohm@0
   477
                         SIMP_TAC (wf_ss' addrews (hyps)) 1) 1);
clasohm@0
   478
clasohm@0
   479
ZF/epsilon/eclose_least: changed ASM_SIMP_TAC to SIMP_TAC; this makes
clasohm@0
   480
METAHYPS version work
clasohm@0
   481
clasohm@0
   482
ZF/arith/add_not_less_self: adds anti_refl_rew
clasohm@0
   483
clasohm@0
   484
ZF/ex/prop-log/hyps_finite: the use of UN_I is very bad -- too undirected.
clasohm@0
   485
Swapping the premises of UN_I would probably allow instantiation.
clasohm@0
   486
clasohm@0
   487
ZF otherwise seems to work!
clasohm@0
   488
clasohm@0
   489
HOL/llist/llistE: loops! due to rewriting by Rep_LList_LCons of Vars
clasohm@0
   490
clasohm@0
   491
HOL/ex/prop-log/comp_lemma: failed due to uninstantiated Var in 
clasohm@0
   492
(CCONTR_rule RS allI)
clasohm@0
   493
clasohm@0
   494
*** REJECTED
clasohm@0
   495
clasohm@0
   496
15 April
clasohm@0
   497
clasohm@0
   498
These overnight runs involve Provers/simp.ML with old treatment of rules
clasohm@0
   499
(match_tac) and no METAHYPS; they test the new flexflex pairs and
clasohm@0
   500
discrimination nets, to see whether it runs faster.
clasohm@0
   501
clasohm@0
   502
MAKE-ALL (NJ 0.93) ran perfectly.  It took 3:39 hours (4 mins faster)
clasohm@0
   503
MAKE-ALL (Poly/ML) ran perfectly.  It took 3:23 hours (5 mins faster)
clasohm@0
   504
clasohm@0
   505
ZF/simpdata/ZF_ss: deleted anti_refl_rew; non-linear patterns slow down
clasohm@0
   506
discrimination nets (and this rewrite used only ONCE)
clasohm@0
   507
clasohm@0
   508
ZF/mem_not_refl: new; replaces obsolete anti_refl_rew
clasohm@0
   509
clasohm@0
   510
**Timing experiments**
clasohm@0
   511
clasohm@0
   512
fun HYP_SIMP_TAC ss = METAHYPS (fn hyps => HOL_SIMP_TAC (ss addrews hyps) 1);
clasohm@0
   513
clasohm@0
   514
On large examples such as ...
clasohm@0
   515
HOL/arith/mod_quo_equality 
clasohm@0
   516
HOL/llist/LListD_implies_ntrunc_equality
clasohm@0
   517
ZF/ex/bin/integ_of_bin_succ
clasohm@0
   518
... it is 1.5 to 3 times faster than ASM_SIMP_TAC.  But cannot replace
clasohm@0
   519
ASM_SIMP_TAC since the auto_tac sometimes fails due to lack of assumptions.
clasohm@0
   520
If there are few assumptions then HYP_SIMP_TAC is no better.
clasohm@0
   521
clasohm@0
   522
Pure/Makefile: now copies $(ML_DBASE) to $(BIN)/Pure instead of calling
clasohm@0
   523
make_database, so that users can call make_database for their object-logics.
clasohm@0
   524
clasohm@0
   525
Pure/tctical/SELECT_GOAL: now does nothing if i=1 and there is
clasohm@0
   526
only one subgoal.
clasohm@0
   527
clasohm@0
   528
19 April
clasohm@0
   529
clasohm@0
   530
MAKE-ALL (NJ 0.93) failed in HOL due to lack of disc space.
clasohm@0
   531
MAKE-ALL (Poly/ML) ran perfectly.  It took 3:23 hours 
clasohm@0
   532
clasohm@0
   533
**** Installation of new simplifier ****
clasohm@0
   534
clasohm@0
   535
Provers/simp/EXEC: now calls METAHYPS and passes the hyps as an extra arg
clasohm@0
   536
to the auto_tac.
clasohm@0
   537
clasohm@0
   538
FOL,HOL/simpdata: auto_tac now handles the hyps argument
clasohm@0
   539
clasohm@0
   540
ZF/simpdata/standard_auto_tac: deleted
clasohm@0
   541
ZF/simpdata/auto_tac: added hyps argument
clasohm@0
   542
ZF/epsilon/eclose_least_lemma: no special auto_tac 
clasohm@0
   543
clasohm@0
   544
*/ex/ROOT: no longer use 'cd' commands; instead pathnames contain "ex/..."
clasohm@0
   545
clasohm@0
   546
20 April
clasohm@0
   547
clasohm@0
   548
MAKE-ALL failed in HOL/Subst
clasohm@0
   549
clasohm@0
   550
HOL/Subst/setplus/cla_case: renamed imp_excluded_middle and simplified.
clasohm@0
   551
Old version caused ambiguity in rewriting:
clasohm@0
   552
     "[| P ==> P-->Q;  ~P ==> ~P-->Q |] ==> Q";
clasohm@0
   553
clasohm@0
   554
**** New tar file placed on /homes/lcp (????) **** 
clasohm@0
   555
clasohm@0
   556
Pure/Syntax: improvements to the printing of syntaxes
clasohm@0
   557
Pure/Syntax/lexicon.ML: added name_of_token
clasohm@0
   558
Pure/Syntax/earley0A.ML: updated print_gram
clasohm@0
   559
clasohm@0
   560
21 April
clasohm@0
   561
clasohm@0
   562
MAKE-ALL (NJ 0.93) ran perfectly.  It took 3:44 hours
clasohm@0
   563
MAKE-ALL (Poly/ML) failed in HOL due to lack of disc space
clasohm@0
   564
clasohm@0
   565
HOL/list,llist: now share NIL, CONS, List_Fun and List_case
clasohm@0
   566
clasohm@0
   567
make-all: now compresses the log files, which were taking up 4M; this
clasohm@0
   568
reduces their space by more than 1/3
clasohm@0
   569
clasohm@0
   570
rm-logfiles: now deletes compressed log files.
clasohm@0
   571
clasohm@0
   572
** Patrick Meche has noted that if the goal is stated with a leading !!
clasohm@0
   573
quantifier, then the list of premises is always empty -- this gives the
clasohm@0
   574
effect of an initial (cut_facts_tac prems 1).  The final theorem is the
clasohm@0
   575
same as it would be without the quantifier.
clasohm@0
   576
clasohm@0
   577
ZF: used the point above to simplify many proofs
clasohm@0
   578
ZF/domrange/cfast_tac: deleted, it simply called cut_facts_tac
clasohm@0
   579
clasohm@0
   580
22 April
clasohm@0
   581
clasohm@0
   582
MAKE-ALL (NJ 0.93) ran perfectly.  It took 3:52 hours??
clasohm@0
   583
MAKE-ALL (Poly/ML) ran perfectly.  It took 3:16 hours
clasohm@0
   584
clasohm@0
   585
30 April
clasohm@0
   586
clasohm@0
   587
HOL: installation of finite set notation: {x1,...,xn} (by Tobias Nipkow)
clasohm@0
   588
clasohm@0
   589
HOL/set.thy,set.ML,fun.ML,equalities.ML: addition of rules for "insert",
clasohm@0
   590
new derivations for "singleton"
clasohm@0
   591
clasohm@0
   592
HOL/llist.thy,llist.ML: changed {x.False} to {}
clasohm@0
   593
clasohm@0
   594
**** New tar file placed on /homes/lcp (584K) **** 
clasohm@0
   595
clasohm@0
   596
4 May
clasohm@0
   597
clasohm@0
   598
MAKE-ALL (NJ 0.93) ran out of space in LK.
clasohm@0
   599
MAKE-ALL (Poly/ML) ran perfectly.  It took 3:14 hours
clasohm@0
   600
clasohm@0
   601
Pure/Makefile: inserted "chmod u+w $(BIN)/Pure;" in case $(ML_DBASE) is
clasohm@0
   602
write-protected
clasohm@0
   603
clasohm@0
   604
5 May
clasohm@0
   605
clasohm@0
   606
HOL/list/not_Cons_self: renamed from l_not_Cons_l
clasohm@0
   607
HOL/list/not_CONS_self: new
clasohm@0
   608
clasohm@0
   609
HOL/llist.thy/Lconst: changed type and def to remove Leaf
clasohm@0
   610
HOL/llist.ML: changed Lconst theorems
clasohm@0
   611
clasohm@0
   612
6 May
clasohm@0
   613
clasohm@0
   614
MAKE-ALL (Poly/ML) ran perfectly.  It took 3:18 hours
clasohm@0
   615
clasohm@0
   616
** Installation of new HOL from Tobias **
clasohm@0
   617
clasohm@0
   618
HOL/ex/{finite,prop-log} made like the ZF versions
clasohm@0
   619
HOL/hol.thy: type classes plus, minus, times; overloaded operators + - *
clasohm@0
   620
HOL/set: set enumeration via "insert"
clasohm@0
   621
         additions to set_cs and set_ss
clasohm@0
   622
HOL/set,subset,equalities: various lemmas to do with {}, insert and -
clasohm@0
   623
HOL/llist: One of the proofs needs one fewer commands
clasohm@0
   624
HOL/arith: many proofs require type constraints due to overloading
clasohm@0
   625
clasohm@0
   626
** end Installation **
clasohm@0
   627
clasohm@0
   628
ZF/ex/misc: added new lemmas from Abrial's paper
clasohm@0
   629
clasohm@0
   630
7 May 
clasohm@0
   631
clasohm@0
   632
HOL/llist.ML/LList_corec_subset1: deleted a fast_tac call; the previous
clasohm@0
   633
simplification now proves the subgoal.
clasohm@0
   634
clasohm@0
   635
**** New tar file placed on /homes/lcp (584K) **** 
clasohm@0
   636
clasohm@0
   637
** Installation of new simplifier from Tobias **
clasohm@0
   638
clasohm@0
   639
The "case_splits" parameter of SimpFun is moved from the signature to the
clasohm@0
   640
simpset.  SIMP_CASE_TAC and ASM_SIMP_CASE_TAC are removed.  The ordinary
clasohm@0
   641
simplification tactics perform case splits if present in the simpset.
clasohm@0
   642
clasohm@0
   643
The simplifier finds out for itself what constant is affected.  Instead of
clasohm@0
   644
supplying the pair (expand_if,"if"), supply just the rule expand_if.
clasohm@0
   645
clasohm@0
   646
This change affects all calls to SIMP_CASE_TAC and all applications of SimpFun.
clasohm@0
   647
clasohm@0
   648
MAKE-ALL (Poly/ML) ran perfectly.  It took 3:18 hours
clasohm@0
   649
clasohm@0
   650
Cube/ex: UNTIL1, UNTIL_THM: replaced by standard tactics DEPTH_SOLVE_1 and
clasohm@0
   651
DEPTH_SOLVE
clasohm@0
   652
clasohm@0
   653
HOL: installation of NORM tag for simplication.  How was it forgotten??
clasohm@0
   654
clasohm@0
   655
HOL/hol.thy: declaration of NORM
clasohm@0
   656
HOL/simpdata: NORM_def supplied to SimpFun
clasohm@0
   657
clasohm@0
   658
10 May
clasohm@0
   659
clasohm@0
   660
MAKE-ALL (Poly/ML) ran perfectly.  It took 3:33 hours??
clasohm@0
   661
clasohm@0
   662
11 May
clasohm@0
   663
clasohm@0
   664
HOL/prod/Prod_eq: renamed Pair_eq
clasohm@0
   665
HOL/ex/lex-prod: wf_lex_prod: simplified proof
clasohm@0
   666
clasohm@0
   667
HOL/fun/inj_eq: new
clasohm@0
   668
clasohm@0
   669
HOL/llist/sumPairE: deleted, thanks to new simplifier's case splits!
clasohm@0
   670
clasohm@0
   671
12 May
clasohm@0
   672
clasohm@0
   673
MAKE-ALL (NJ 0.93) ran out of space in HOL.
clasohm@0
   674
MAKE-ALL (Poly/ML) failed in HOL.
clasohm@0
   675
HOL/Subst/utermlemmas/utlemmas_ss: deleted Prod_eq from the congruence rules
clasohm@0
   676
clasohm@0
   677
13 May
clasohm@0
   678
clasohm@0
   679
Pure/logic/flexpair: moved to term, with "equals" etc.  Now pervasive
clasohm@0
   680
Pure/logic/mk_flexpair: now exported
clasohm@0
   681
Pure/logic/dest_flexpair: new
clasohm@0
   682
Pure/goals/print_exn: now prints the error message for TERM and TYPE
clasohm@0
   683
clasohm@0
   684
Pure/Syntax/sextension: now =?= has type ['a::{}, 'a] => prop because
clasohm@0
   685
flexflex pairs can have any type at all.  Thus == must have the same type.
clasohm@0
   686
clasohm@0
   687
Pure/thm/flexpair_def: now =?= and == are equated for all 'a::{}.
clasohm@0
   688
clasohm@0
   689
Pure/tctical/equal_abs_elim,equal_abs_elim_list: new (for METAHYPS fix)
clasohm@0
   690
Pure/tctical/METAHYPS: now works if new proof state has flexflex pairs
clasohm@0
   691
clasohm@0
   692
Pure/Syntax/earley0A,syntax,lexicon: Tokens are represented by strings now,
clasohm@0
   693
not by integers.  (Changed by Tobias)
clasohm@0
   694
clasohm@0
   695
*** Installation of more printing functions ***
clasohm@0
   696
clasohm@0
   697
Pure/sign/sg: changed from a type abbrev to a datatype
clasohm@0
   698
Pure/type/type_sig: changed from a type abbrev to a datatype
clasohm@0
   699
These changes needed for abstract type printing in NJ
clasohm@0
   700
clasohm@0
   701
Pure/tctical/print_sg,print_theory: new
clasohm@0
   702
clasohm@0
   703
Pure/drule: new file containing derived rules and printing functions.
clasohm@0
   704
Mostly from tctical.ML, but includes rewriting rules from tactic.ML.
clasohm@0
   705
clasohm@0
   706
Pure/ROOT: loads drule before tctical; TacticalFun,TacticFun,GoalsFun now
clasohm@0
   707
depend on Drule and have sharing constraints.
clasohm@0
   708
clasohm@0
   709
14 May
clasohm@0
   710
clasohm@0
   711
Installing new print functions for New Jersey: incompatible with Poly/ML!
clasohm@0
   712
clasohm@0
   713
Pure/NJ/install_pp_nj: new (requires datatypes as above)
clasohm@0
   714
Pure/POLY/install_pp_nj: a dummy version
clasohm@0
   715
clasohm@0
   716
Pure/ROOT: calls install_pp_nj to install printing for NJ
clasohm@0
   717
clasohm@0
   718
*/ROOT: added extra install_pp calls (sg, theory, cterm, typ, ctyp) for
clasohm@0
   719
Poly/ML [ZF,LCF,Modal do not need them since they inherit them from another
clasohm@0
   720
logic -- make_database is not used]
clasohm@0
   721
clasohm@0
   722
17 May
clasohm@0
   723
clasohm@0
   724
MAKE-ALL (NJ 0.93) ran perfectly.  It took 3:57 hours??
clasohm@0
   725
clasohm@0
   726
Pure/Syntax/lexicon: Yet another leaner and faster version ... (from Tobias)
clasohm@0
   727
clasohm@0
   728
18 May
clasohm@0
   729
clasohm@0
   730
MAKE-ALL (Poly/ML) ran perfectly.  It took 3:36 hours
clasohm@0
   731
clasohm@0
   732
19 May
clasohm@0
   733
clasohm@0
   734
ZF/equalities/Union_singleton,Inter_singleton: now refer to {b} instead of
clasohm@0
   735
complex assumptions
clasohm@0
   736
clasohm@0
   737
20 May
clasohm@0
   738
clasohm@0
   739
HOL/list: Tobias added the [x1,...,xn] notation and the functions hd, tl,
clasohm@0
   740
null and list_case.
clasohm@0
   741
clasohm@0
   742
1 June
clasohm@0
   743
clasohm@0
   744
MAKE-ALL (Poly/ML) ran perfectly.  It took 3:39 hours
clasohm@0
   745
clasohm@0
   746
**** New tar file 92.tar.z placed on /homes/lcp (376K) **** 
clasohm@0
   747
clasohm@0
   748
MAKE-ALL (NJ 0.93) ran perfectly.  It took 1:49 hours on albatross.
clasohm@0
   749
clasohm@0
   750
Pure/tactic/dres_inst_tac,forw_inst_tac: now call the new
clasohm@0
   751
make_elim_preserve to preserve Var indexes when creating the elimination
clasohm@0
   752
rule.
clasohm@0
   753
clasohm@0
   754
ZF/ex/ramsey: modified calls to dres_inst_tac
clasohm@0
   755
clasohm@0
   756
2 June
clasohm@0
   757
clasohm@0
   758
Pure/Thy/read/read_thy,use_thy: the .thy.ML file is now written to the
clasohm@0
   759
current directory, since the pathname may lead to a non-writeable area.
clasohm@0
   760
clasohm@0
   761
HOL/arith: renamed / and // to div and mod
clasohm@0
   762
ZF/arith: renamed #/ and #// to div and mod
clasohm@0
   763
clasohm@0
   764
MAKE-ALL (Poly/ML) ran perfectly.  It took 1:48 hours on albatross.
clasohm@0
   765
clasohm@0
   766
**** New tar file 92.tar.z placed on /homes/lcp (376K) **** 
clasohm@0
   767
clasohm@0
   768
Pure/NJ/commit: new dummy function
clasohm@0
   769
FOLP/ex/ROOT: inserted commit call to avoid Poly/ML problems
clasohm@0
   770
clasohm@0
   771
make-all: now builds FOLP also!
clasohm@0
   772
clasohm@0
   773
3 June
clasohm@0
   774
clasohm@0
   775
ZF/zf.thy,HOL/list.thy,HOL/set.thy: now constructions involving {_}, [_],
clasohm@0
   776
<_,_> are formatted as {(_)}, [(_)], 
clasohm@0
   777
clasohm@0
   778
MAKE-ALL (Poly/ML) ran perfectly.  It took 4:37 hours on muscovy (with FOLP).
clasohm@0
   779
clasohm@0
   780
ZF/Makefile: removed obsolete target for .rules.ML
clasohm@0
   781
clasohm@0
   782
All object-logic Makefiles: EXAMPLES ARE NO LONGER SAVED.  This saves disc
clasohm@0
   783
and avoids problems (in New Jersey ML) of writing to the currently
clasohm@0
   784
executing image.
clasohm@0
   785
clasohm@0
   786
4 June
clasohm@0
   787
clasohm@0
   788
Pure/logic/rewritec: now uses nets for greater speed.  Functor LogicFun now
clasohm@0
   789
takes Net as argument.
clasohm@0
   790
clasohm@0
   791
Pure/ROOT: now loads net before logic.
clasohm@0
   792
clasohm@0
   793
MAKE-ALL (Poly/ML) failed in ZF and HOL.
clasohm@0
   794
clasohm@0
   795
LK/lk.thy: changed constant "not" to "Not" (for consistency with FOL)
clasohm@0
   796
clasohm@0
   797
7 June
clasohm@0
   798
clasohm@0
   799
Pure/tactic/is_letdig: moved to library
clasohm@0
   800
Pure/Syntax/lexicon/is_qld: deleted, was same as is_letdig
clasohm@0
   801
clasohm@0
   802
MAKE-ALL (Poly/ML) ran perfectly.  It took 2:07 hours on albatross.
clasohm@0
   803
MAKE-ALL (NJ 0.93) ran perfectly.  It took 4:41 hours on dunlin.
clasohm@0
   804
clasohm@0
   805
HOL/set/UN1,INT1: new union/intersection operators.  Binders UN x.B(x),
clasohm@0
   806
INT x.B(x).
clasohm@0
   807
clasohm@0
   808
HOL/univ,llist: now use UN x.B(x) instead of Union(range(B))
clasohm@0
   809
clasohm@0
   810
HOL/subset: added lattice properties for INT, UN (both forms)
clasohm@0
   811
clasohm@0
   812
8 June
clasohm@0
   813
clasohm@0
   814
MAKE-ALL (NJ 0.93) ran perfectly.  It took 4:45 hours on dunlin.
clasohm@0
   815
clasohm@0
   816
**** New tar file 92.tar.z placed on /homes/lcp (384K) **** 
clasohm@0
   817
clasohm@0
   818
14 June
clasohm@0
   819
clasohm@0
   820
HOL/list.thy/List_rec_def: changed pred_sexp (a variable!) to pred_Sexp.
clasohm@0
   821
Using def_wfrec hides such errors!!
clasohm@0
   822
clasohm@0
   823
**** New tar file 92.tar.gz placed on /homes/lcp (384K) **** 
clasohm@0
   824
clasohm@0
   825
** NEW VERSION FROM MUNICH WITH ==-REWRITING **
clasohm@0
   826
clasohm@0
   827
** The following changes are Toby's **
clasohm@0
   828
clasohm@0
   829
type.ML:
clasohm@0
   830
clasohm@0
   831
Renamed mark_free to freeze_vars and thaw_tvars to thaw_vars.
clasohm@0
   832
Added both functions to the signature.
clasohm@0
   833
clasohm@0
   834
sign.ML:
clasohm@0
   835
clasohm@0
   836
Added val subsig: sg * sg -> bool to signature.
clasohm@0
   837
Added trueprop :: prop and mark_prop : prop => prop to pure_sg.
clasohm@0
   838
clasohm@0
   839
Added
clasohm@0
   840
clasohm@0
   841
val freeze_vars: term -> term
clasohm@0
   842
val thaw_vars: term -> term
clasohm@0
   843
val strip_all_imp: term * int -> term list * term * int
clasohm@0
   844
clasohm@0
   845
Moved rewritec_bottom and rewritec_top to thm.ML.
clasohm@0
   846
Only bottom-up rewriting supported any longer.
clasohm@0
   847
clasohm@0
   848
thm.ML:
clasohm@0
   849
clasohm@0
   850
Added
clasohm@0
   851
clasohm@0
   852
(* internal form of conditional ==-rewrite rules *)
clasohm@0
   853
type meta_simpset
clasohm@0
   854
val add_mss: meta_simpset * thm list -> meta_simpset
clasohm@0
   855
val empty_mss: meta_simpset
clasohm@0
   856
val mk_mss: thm list -> meta_simpset
clasohm@0
   857
clasohm@0
   858
val mark_prop_def: thm
clasohm@0
   859
val truepropI: thm
clasohm@0
   860
val trueprop_def: thm
clasohm@0
   861
clasohm@0
   862
(* bottom-up conditional ==-rewriting with local ==>-assumptions *)
clasohm@0
   863
val rewrite_cterm: meta_simpset -> (thm -> thm list)
clasohm@0
   864
                   -> (meta_simpset -> thm list -> Sign.cterm -> thm)
clasohm@0
   865
                   -> Sign.cterm -> thm
clasohm@0
   866
val trace_simp: bool ref
clasohm@0
   867
clasohm@0
   868
Simplified concl_of: call to Logic.skip_flexpairs redundant.
clasohm@0
   869
clasohm@0
   870
drule.ML:
clasohm@0
   871
clasohm@0
   872
Added
clasohm@0
   873
clasohm@0
   874
(* rewriting *)
clasohm@0
   875
val asm_rewrite_rule: (thm -> thm list) -> thm list -> thm -> thm
clasohm@0
   876
val rewrite_goal_rule: (thm -> thm list) -> thm list -> int -> thm -> thm
clasohm@0
   877
val rewrite_goals_rule: (thm -> thm list) -> thm list -> thm -> thm
clasohm@0
   878
clasohm@0
   879
(* derived concepts *)
clasohm@0
   880
val forall_trueprop_eq: thm
clasohm@0
   881
val implies_trueprop_eq: thm
clasohm@0
   882
val mk_trueprop_eq: thm -> thm
clasohm@0
   883
val reflexive_eq: thm
clasohm@0
   884
val reflexive_thm: thm
clasohm@0
   885
val trueprop_implies_eq: thm
clasohm@0
   886
val thm_implies: thm -> thm -> thm
clasohm@0
   887
val thm_equals: thm -> thm -> thm
clasohm@0
   888
clasohm@0
   889
(*Moved here from tactic.ML:*)
clasohm@0
   890
val asm_rl: thm
clasohm@0
   891
val cut_rl: thm
clasohm@0
   892
val revcut_rl: thm
clasohm@0
   893
clasohm@0
   894
tactic.ML:
clasohm@0
   895
clasohm@0
   896
Added
clasohm@0
   897
clasohm@0
   898
val asm_rewrite_goal_tac: (thm -> thm list) -> thm list -> int -> tactic
clasohm@0
   899
val asm_rewrite_goals_tac: (thm -> thm list) -> thm list -> tactic
clasohm@0
   900
val asm_rewrite_tac: (thm -> thm list) -> thm list -> tactic
clasohm@0
   901
val fold_goal_tac: thm list -> int -> tactic
clasohm@0
   902
val rewrite_goal_tac: thm list -> int -> tactic
clasohm@0
   903
clasohm@0
   904
Moved to drule.ML:
clasohm@0
   905
val asm_rl: thm
clasohm@0
   906
val cut_rl: thm
clasohm@0
   907
val revcut_rl: thm
clasohm@0
   908
clasohm@0
   909
goals.ML:
clasohm@0
   910
clasohm@0
   911
Changed prepare_proof to make sure that rewriting with empty list of
clasohm@0
   912
meta-thms is identity.
clasohm@0
   913
clasohm@0
   914
** End of Toby's changes **
clasohm@0
   915
clasohm@0
   916
16 June
clasohm@0
   917
clasohm@0
   918
Pure/sign/typ_of,read_ctyp: new
clasohm@0
   919
Pure/logic/dest_flexpair: now exported
clasohm@0
   920
clasohm@0
   921
Pure/drule/flexpair_intr,flexpair_elim: new; fixes a bug in
clasohm@0
   922
flexpair_abs_elim_list
clasohm@0
   923
clasohm@0
   924
HOL/equalities/image_empty,image_insert: new
clasohm@0
   925
HOL/ex/finite/Fin_imageI: new
clasohm@0
   926
clasohm@0
   927
Installed Martin Coen's CCL as new object-logic
clasohm@0
   928
clasohm@0
   929
17 June
clasohm@0
   930
clasohm@0
   931
** More changes from Munich (Markus Wenzel) **
clasohm@0
   932
clasohm@0
   933
Pure/library: added the, is_some, is_none, separate and improved space_implode
clasohm@0
   934
Pure/sign: Sign.extend now calls Syntax.extend with list of constants
clasohm@0
   935
Pure/symtab: added is_null
clasohm@0
   936
Pure/Syntax/sextension: added empty_sext
clasohm@0
   937
Pure/Syntax/syntax: changed Syntax.extend for compatibility with future version
clasohm@0
   938
clasohm@0
   939
HOL now exceeds poly's default heap size. Hence HOL/Makefile needs to
clasohm@0
   940
specify -h 8000.
clasohm@0
   941
clasohm@0
   942
HOL/univ/ntrunc_subsetD, etc: deleted the useless j<k assumption
clasohm@0
   943
clasohm@0
   944
18 June
clasohm@0
   945
clasohm@0
   946
MAKE-ALL (Poly/ML) ran perfectly.  It took 4:59 hours on dunlin (with CCL).
clasohm@0
   947
clasohm@0
   948
Pure/sign/read_def_cterm: now prints the offending terms, as well as the
clasohm@0
   949
types, when exception TYPE is raised.
clasohm@0
   950
clasohm@0
   951
HOL/llist: some tidying
clasohm@0
   952
clasohm@0
   953
23 June
clasohm@0
   954
clasohm@0
   955
HOL/llist/Lconst_type: generalized from Lconst(M): LList({M})
clasohm@0
   956
clasohm@0
   957
24 June
clasohm@0
   958
clasohm@0
   959
MAKE-ALL (Poly/ML) ran perfectly.  It took 2:23 hours on albatross (with CCL)
clasohm@0
   960
clasohm@0
   961
MAKE-ALL (NJ 0.93) failed in CCL due to use of "abstraction" as an
clasohm@0
   962
identifier in CCL.ML
clasohm@0
   963
clasohm@0
   964
**** New tar file 92.tar.gz placed on /homes/lcp (384K) **** (with CCL)
clasohm@0
   965
clasohm@0
   966
CCL/ROOT: added ".ML" extension to use commands for NJ compatibility
clasohm@0
   967
clasohm@0
   968
25 June
clasohm@0
   969
clasohm@0
   970
MAKE-ALL (Poly/ML) ran perfectly.  It took 2:23 hours on albatross.
clasohm@0
   971
MAKE-ALL (NJ 0.93) failed in HOL due to lack of ".ML" extension
clasohm@0
   972
clasohm@0
   973
HOL/fun/rangeE,imageE: eta-expanded f to get variable name preservation
clasohm@0
   974
clasohm@0
   975
HOL/llist/iterates_equality,lmap_lappend_distrib: tidied
clasohm@0
   976
clasohm@0
   977
28 June
clasohm@0
   978
clasohm@0
   979
HOL/set/UN1_I: made the Var and Bound variables agree ("x") to get variable
clasohm@0
   980
name preservation 
clasohm@0
   981
clasohm@0
   982
HOL/llist: co-induction rules applied with res_inst_tac to state the
clasohm@0
   983
bisimulation directly
clasohm@0
   984
clasohm@0
   985
2 July
clasohm@0
   986
clasohm@0
   987
MAKE-ALL (NJ 0.93) ran perfectly.  It took 2:10 hours on albatross.
clasohm@0
   988
MAKE-ALL (Poly/ML) ran perfectly.  It took 2:23 hours on albatross.
clasohm@0
   989
clasohm@0
   990
92/Makefile/$(BIN)/Pure: changed echo makefile= to echo database=
clasohm@0
   991
clasohm@0
   992
**** New tar file 92.tar.gz placed on /homes/lcp (424K) **** (with CCL)
clasohm@0
   993
clasohm@0
   994
clasohm@0
   995
** NEW VERSION FROM MUNICH WITH ABSTRACT SYNTAX TREES & NEW PARSER **
clasohm@0
   996
clasohm@0
   997
I have merged in the changes shown above since 24 June
clasohm@0
   998
clasohm@0
   999
CHANGES LOG OF Markus Wenzel (MMW)
clasohm@0
  1000
=======
clasohm@0
  1001
clasohm@0
  1002
29-Jun-1993 MMW
clasohm@0
  1003
  *** Beta release of new syntax module ***
clasohm@0
  1004
  (should be 99% backwards compatible)
clasohm@0
  1005
clasohm@0
  1006
  Pure/Thy/ROOT.ML
clasohm@0
  1007
    added keywords for "translations" section
clasohm@0
  1008
clasohm@0
  1009
  Pure/Thy/syntax.ML
clasohm@0
  1010
    minor cleanup
clasohm@0
  1011
    added syntax for "translations" section
clasohm@0
  1012
    .*.thy.ML files now human readable
clasohm@0
  1013
    .*.thy.ML used to be generated incorrectly if no mixfix but "ML" section
clasohm@0
  1014
    "ML" section no longer demands any definitions (parse_translation, ...)
clasohm@0
  1015
clasohm@0
  1016
  Pure/Thy/read.ML
clasohm@0
  1017
    read_thy: added close_in
clasohm@0
  1018
    added file_exists (not perfect)
clasohm@0
  1019
    use_thy: now uses file_exists
clasohm@0
  1020
clasohm@0
  1021
  Pure/thm.ML
clasohm@0
  1022
    added syn_of: theory -> syntax
clasohm@0
  1023
clasohm@0
  1024
  Pure/Makefile
clasohm@0
  1025
    SYNTAX_FILES: added Syntax/ast.ML
clasohm@0
  1026
clasohm@0
  1027
  Pure/Syntax/pretty.ML
clasohm@0
  1028
    added str_of: T -> string
clasohm@0
  1029
clasohm@0
  1030
  Pure/Syntax/ast.ML
clasohm@0
  1031
    added this file
clasohm@0
  1032
clasohm@0
  1033
  Pure/Syntax/extension.ML
clasohm@0
  1034
  Pure/Syntax/parse_tree.ML
clasohm@0
  1035
  Pure/Syntax/printer.ML
clasohm@0
  1036
  Pure/Syntax/ROOT.ML
clasohm@0
  1037
  Pure/Syntax/sextension.ML
clasohm@0
  1038
  Pure/Syntax/syntax.ML
clasohm@0
  1039
  Pure/Syntax/type_ext.ML
clasohm@0
  1040
  Pure/Syntax/xgram.ML
clasohm@0
  1041
    These files have been completely rewritten, though the global structure
clasohm@0
  1042
    is similar to the old one.
clasohm@0
  1043
clasohm@0
  1044
clasohm@0
  1045
30-Jun-1993 MMW
clasohm@0
  1046
  New versions of HOL and Cube: use translation rules wherever possible;
clasohm@0
  1047
clasohm@0
  1048
  HOL/hol.thy
clasohm@0
  1049
    cleaned up
clasohm@0
  1050
    removed alt_tr', mk_bindopt_tr'
clasohm@0
  1051
    alternative binders now implemented via translation rules and mk_alt_ast_tr'
clasohm@0
  1052
clasohm@0
  1053
  HOL/set.thy
clasohm@0
  1054
    cleaned up
clasohm@0
  1055
    removed type "finset"
clasohm@0
  1056
    now uses category "args" for finite sets
clasohm@0
  1057
    junked "ML" section
clasohm@0
  1058
    added "translations" section
clasohm@0
  1059
clasohm@0
  1060
  HOL/list.thy
clasohm@0
  1061
    cleaned up
clasohm@0
  1062
    removed type "listenum"
clasohm@0
  1063
    now uses category "args" for lists
clasohm@0
  1064
    junked "ML" section
clasohm@0
  1065
    added "translations" section
clasohm@0
  1066
clasohm@0
  1067
  Cube/cube.thy
clasohm@0
  1068
    cleaned up
clasohm@0
  1069
    changed indentation of Lam and Pi from 2 to 3
clasohm@0
  1070
    removed qnt_tr, qnt_tr', no_asms_tr, no_asms_tr'
clasohm@0
  1071
    fixed fun_tr': all but one newly introduced frees will have type dummyT
clasohm@0
  1072
    added "translations" section
clasohm@0
  1073
clasohm@0
  1074
clasohm@0
  1075
30-Jun-1993, 05-Jul-1993 MMW
clasohm@0
  1076
  Improved toplevel pretty printers:
clasohm@0
  1077
    - unified interface for POLY and NJ;
clasohm@0
  1078
    - print functions now insert atomic string into the toplevel's pp stream,
clasohm@0
  1079
      rather than writing it to std_out (advantage: output appears at the
clasohm@0
  1080
      correct position, disadvantage: output cannot be broken);
clasohm@0
  1081
  (Is there anybody in this universe who exactly knows how Poly's install_pp
clasohm@0
  1082
  is supposed to work?);
clasohm@0
  1083
clasohm@0
  1084
  Pure/NJ.ML
clasohm@0
  1085
    removed dummy install_pp
clasohm@0
  1086
    added make_pp, install_pp
clasohm@0
  1087
clasohm@0
  1088
  Pure/POLY.ML
clasohm@0
  1089
    removed dummy install_pp_nj
clasohm@0
  1090
    added make_pp
clasohm@0
  1091
clasohm@0
  1092
  Pure/ROOT.ML
clasohm@0
  1093
    removed install_pp_nj stuff
clasohm@0
  1094
clasohm@0
  1095
  Pure/drule.ML
clasohm@0
  1096
    added str_of_sg, str_of_theory, str_of_thm
clasohm@0
  1097
clasohm@0
  1098
  Pure/install_pp.ML
clasohm@0
  1099
    added this file
clasohm@0
  1100
clasohm@0
  1101
  Pure/sign.ML
clasohm@0
  1102
    added str_of_term, str_of_typ, str_of_cterm, str_of_ctyp
clasohm@0
  1103
clasohm@0
  1104
  Pure/goals.ML
clasohm@0
  1105
    added str_of_term, str_of_typ
clasohm@0
  1106
clasohm@0
  1107
  CTT/ROOT.ML
clasohm@0
  1108
  Cube/ROOT.ML
clasohm@0
  1109
  FOL/ROOT.ML
clasohm@0
  1110
  FOLP/ROOT.ML
clasohm@0
  1111
  HOL/ROOT.ML
clasohm@0
  1112
  LK/ROOT.ML
clasohm@0
  1113
    replaced install_pp stuff by 'use "../Pure/install_pp.ML"'
clasohm@0
  1114
clasohm@0
  1115
clasohm@0
  1116
01-Jul-1993 MMW
clasohm@0
  1117
  Misc small fixes
clasohm@0
  1118
clasohm@0
  1119
  CCL/ROOT.ML
clasohm@0
  1120
  HOL/ROOT.ML
clasohm@0
  1121
    added ".ML" suffix to some filenames
clasohm@0
  1122
clasohm@0
  1123
  HOL/ex/unsolved.ML
clasohm@0
  1124
    replaced HOL_Rule.thy by HOL.thy
clasohm@0
  1125
clasohm@0
  1126
  Pure/NJ.ML
clasohm@0
  1127
    quit was incorrectly int -> unit
clasohm@0
  1128
clasohm@0
  1129
END MMW CHANGES
clasohm@0
  1130
clasohm@0
  1131
Pure/Syntax/sextension/eta_contract: now initially false 
clasohm@0
  1132
clasohm@0
  1133
Pure/library/cat_lines: no longer calls "distinct"
clasohm@0
  1134
Pure/sign: replaced to calls of implode (map (apr(op^,"\n") o ... by cat_lines
clasohm@0
  1135
NB This could cause duplicate error messages from Pure/sign and Pure/type
clasohm@0
  1136
clasohm@0
  1137
Pure/goals/prove_goalw: now prints some of the information from print_exn
clasohm@0
  1138
clasohm@0
  1139
9 July
clasohm@0
  1140
clasohm@0
  1141
MAKE-ALL (Poly/ML) ran perfectly.  It took 2:26 hours on albatross.
clasohm@0
  1142
clasohm@0
  1143
**** New tar file 93.tar.gz placed on /homes/lcp (480K) **** 
clasohm@0
  1144
clasohm@0
  1145
12 July
clasohm@0
  1146
clasohm@0
  1147
MAKE-ALL (NJ 0.93) ran perfectly.  It took 2:13 hours on albatross.
clasohm@0
  1148
MAKE-ALL (Poly/ML) ran perfectly.  It took 2:25 hours on albatross.
clasohm@0
  1149
clasohm@0
  1150
22 July
clasohm@0
  1151
clasohm@0
  1152
ZF/zf.thy: new version from Marcus Wenzel
clasohm@0
  1153
clasohm@0
  1154
ZF: ** installation of inductive definitions **
clasohm@0
  1155
clasohm@0
  1156
changing the argument order of "split"; affects fst/snd too
clasohm@0
  1157
sum.thy zf.thy ex/bin.thy ex/integ.thy ex/simult.thy ex/term.thy
clasohm@0
  1158
pair.ML  ex/integ.ML
clasohm@0
  1159
clasohm@0
  1160
changing the argument order of "case" and adding "Part": sum.thy sum.ML
clasohm@0
  1161
clasohm@0
  1162
ZF/zf.ML/rev_subsetD,rev_bspec: new
clasohm@0
  1163
clasohm@0
  1164
ZF/mono: new rules for implication
clasohm@0
  1165
ZF/mono/Collect_mono: now for use with implication rules
clasohm@0
  1166
clasohm@0
  1167
ZF/zf.ML/ballE': renamed rev_ballE
clasohm@0
  1168
clasohm@0
  1169
ZF/list.thy,list.ML: files renamed list-fn.thy, list-fn.ML
clasohm@0
  1170
ZF/list.ML: new version simply holds the datatype definition
clasohm@0
  1171
NB THE LIST CONSTRUCTORS ARE NOW Nil/Cons, not 0/Pair.
clasohm@0
  1172
clasohm@0
  1173
ZF/extend_ind.ML, datatype.ML: new files
clasohm@0
  1174
ZF/fin.ML: moved from ex/finite.ML
clasohm@0
  1175
clasohm@0
  1176
23 July
clasohm@0
  1177
clasohm@0
  1178
ZF/ex/sexp: deleted this example -- it seems hardly worth the trouble of
clasohm@0
  1179
porting.
clasohm@0
  1180
clasohm@0
  1181
ZF/ex/bt.thy,bt.ML: files renamed bt-fn.thy, bt-fn.ML
clasohm@0
  1182
ZF/ex/bt.ML: new version simply holds the datatype definition
clasohm@0
  1183
clasohm@0
  1184
ZF/ex/term.thy,term.ML: files renamed term-fn.thy, term-fn.ML
clasohm@0
  1185
ZF/ex/term.ML: new version simply holds the datatype definition
clasohm@0
  1186
clasohm@0
  1187
ZF/sum/InlI,InrI: renamed from sum_InlI, sum_InlI
clasohm@0
  1188
clasohm@0
  1189
26 July
clasohm@0
  1190
clasohm@0
  1191
ZF/univ/rank_ss: new, for proving recursion equations
clasohm@0
  1192
clasohm@0
  1193
ZF/domrange/image_iff,image_singleton_iff,vimage_iff,vimage_singleton_iff,
clasohm@0
  1194
field_of_prod:new
clasohm@0
  1195
clasohm@0
  1196
ZF/domrange/field_subset: modified
clasohm@0
  1197
clasohm@0
  1198
ZF/list/list_cases: no longer proved by induction!
clasohm@0
  1199
ZF/wf/wf_trancl: simplified proof
clasohm@0
  1200
clasohm@0
  1201
ZF/equalities: new laws for field
clasohm@0
  1202
clasohm@0
  1203
29 July
clasohm@0
  1204
clasohm@0
  1205
ZF/trancl/trancl_induct: new
clasohm@0
  1206
ZF/trancl/rtrancl_induct,trancl_induct: now with more type information
clasohm@0
  1207
clasohm@0
  1208
** More changes from Munich (Markus Wenzel) **
clasohm@0
  1209
clasohm@0
  1210
Update of new syntax module (aka macro system): mostly internal cleanup and
clasohm@0
  1211
polishing;
clasohm@0
  1212
clasohm@0
  1213
  Pure/Syntax/*
clasohm@0
  1214
    added Ast.stat_norm
clasohm@0
  1215
    added Syntax.print_gram, Syntax.print_trans, Syntax.print_syntax
clasohm@0
  1216
    cleaned type and Pure syntax: "_CLASSES" -> "classes", "_SORTS" -> "sorts",
clasohm@0
  1217
     "_==>" -> "==>", "_fun" -> "fun", added some space for printing
clasohm@0
  1218
    Printer: partial fix of the "PROP <aprop>" problem: print "PROP " before
clasohm@0
  1219
      any Var or Free of type propT
clasohm@0
  1220
    Syntax: added ndependent_tr, dependent_tr'
clasohm@0
  1221
clasohm@0
  1222
  Pure/sign.ML: removed declaration of "==>" (now in Syntax.pure_sext)
clasohm@0
  1223
clasohm@0
  1224
Changes to object logics: minor cleanups and replacement of most remaining ML
clasohm@0
  1225
translations by rewrite rules (see also file "Translations");
clasohm@0
  1226
clasohm@0
  1227
  ZF/zf.thy
clasohm@0
  1228
    added "translations" section
clasohm@0
  1229
    removed all parse/print translations except ndependent_tr, dependent_tr'
clasohm@0
  1230
    fixed dependent_tr': all but one newly introduced frees have type dummyT
clasohm@0
  1231
    replaced id by idt in order to make terms rereadable if !show_types
clasohm@0
  1232
clasohm@0
  1233
  Cube/cube.thy
clasohm@0
  1234
    removed necontext
clasohm@0
  1235
    replaced fun_tr/tr' by ndependent_tr/dependent_tr'
clasohm@0
  1236
clasohm@0
  1237
  CTT/ctt.thy
clasohm@0
  1238
    added translations rules for PROD and SUM
clasohm@0
  1239
    removed dependent_tr
clasohm@0
  1240
    removed definitions of ndependent_tr, dependent_tr'
clasohm@0
  1241
clasohm@0
  1242
  HOL/set.thy: replaced id by idt
clasohm@0
  1243
clasohm@0
  1244
  CCL/ROOT.ML: Logtic -> Logic
clasohm@0
  1245
clasohm@0
  1246
  CCL/set.thy
clasohm@0
  1247
    added "translations" section
clasohm@0
  1248
    removed "ML" section
clasohm@0
  1249
    replaced id by idt
clasohm@0
  1250
clasohm@0
  1251
  CCL/types.thy
clasohm@0
  1252
    added "translations" section
clasohm@0
  1253
    removed definitions of ndependent_tr, dependent_tr'
clasohm@0
  1254
    replaced id by idt
clasohm@0
  1255
clasohm@0
  1256
Yet another improvement of toplevel pretty printers: output now breakable;
clasohm@0
  1257
clasohm@0
  1258
  Pure/NJ.ML Pure/POLY.ML improved make_pp
clasohm@0
  1259
clasohm@0
  1260
  Pure/install_pp.ML: replaced str_of_* by pprint_*
clasohm@0
  1261
clasohm@0
  1262
  Pure/drule.ML: replaced str_of_{sg,theory,thm} by pprint_*
clasohm@0
  1263
clasohm@0
  1264
  Pure/sign.ML: replaced str_of_{term,typ,cterm,ctyp} by pprint_*
clasohm@0
  1265
clasohm@0
  1266
  Pure/goals.ML: fixed and replaced str_of_{term,typ} by pprint_*
clasohm@0
  1267
clasohm@0
  1268
  Pure/Syntax/pretty.ML: added pprint, quote
clasohm@0
  1269
clasohm@0
  1270
Minor changes and additions;
clasohm@0
  1271
clasohm@0
  1272
  Pure/sign.ML: renamed stamp "PURE" to "Pure"
clasohm@0
  1273
clasohm@0
  1274
  Pure/library.ML
clasohm@0
  1275
    added quote: string -> string
clasohm@0
  1276
    added to_lower: string -> bool
clasohm@0
  1277
clasohm@0
  1278
  Pure/NJ.ML,POLY.ML: added file_info of Carsten Clasohm
clasohm@0
  1279
clasohm@0
  1280
30 July
clasohm@0
  1281
clasohm@0
  1282
MAKE-ALL (Poly/ML) ran perfectly.
clasohm@0
  1283
clasohm@0
  1284
Pure/goals/print_sign_exn: new, takes most code from print_exn
clasohm@0
  1285
Pure/goals/prove_goalw: displays exceptions using print_sign_exn
clasohm@0
  1286
clasohm@0
  1287
Pure/drule/print_sg: now calls pretty_sg to agree with pprint_sg
clasohm@0
  1288
clasohm@0
  1289
Pure/library,...: replaced front/nth_tail by take/drop.
clasohm@0
  1290
clasohm@0
  1291
Pure/term/typ_tfrees,typ_tvars,term_tfrees,term_tvars: new
clasohm@0
  1292
thm/mk_rew_triple, drule/types_sorts, sign/zero_tvar_indices: now use the above
clasohm@0
  1293
clasohm@0
  1294
Pure/logic/add_term_vars,add_term_frees,insert_aterm,atless:
clasohm@0
  1295
moved to term, joining similar functions for type variables;
clasohm@0
  1296
Logic.vars and Logic.frees are now term_vars and term_frees
clasohm@0
  1297
clasohm@0
  1298
Pure/term/subst_free: new
clasohm@0
  1299
clasohm@0
  1300
Pure/tactic/is_fact: newly exported
clasohm@0
  1301
clasohm@0
  1302
Provers/simp/mk_congs: uses filter_out is_fact to delete trivial cong rules
clasohm@0
  1303
clasohm@0
  1304
Pure/tactic/rename_last_tac: now uses Syntax.is_identifier instead of
clasohm@0
  1305
forall is_letdig
clasohm@0
  1306
clasohm@0
  1307
**** New tar file 93.tar.gz placed on /homes/lcp (448K) **** 
clasohm@0
  1308
clasohm@0
  1309
2 August
clasohm@0
  1310
clasohm@0
  1311
MAKE-ALL (NJ 0.93) failed in ZF due to Compiler bug: elabDecl:open:FctBodyStr
clasohm@0
  1312
MAKE-ALL (Poly/ML) failed in ZF/enum.  It took 2:33 hours on albatross.
clasohm@0
  1313
clasohm@0
  1314
Pure/drule/triv_forall_equality: new
clasohm@0
  1315
Pure/tactic/prune_params_tac: new
clasohm@0
  1316
clasohm@0
  1317
Provers/hypsubst/bound_hyp_subst_tac: new, safer than hyp_subst_tac
clasohm@0
  1318
clasohm@0
  1319
3 August
clasohm@0
  1320
clasohm@0
  1321
Pure/tactic/rule_by_tactic: new
clasohm@0
  1322
clasohm@0
  1323
ZF/perm/compEpair: now proved via rule_by_tactic
clasohm@0
  1324
clasohm@0
  1325
ZF/extend_ind/cases,mk_cases: new
clasohm@0
  1326
ZF/datatype/mk_free: new
clasohm@0
  1327
ZF/list: now calls List.mk_cases
clasohm@0
  1328
clasohm@0
  1329
4 August
clasohm@0
  1330
clasohm@0
  1331
Provers/slow_tac,slow_best_tac: new
clasohm@0
  1332
clasohm@0
  1333
5 August
clasohm@0
  1334
clasohm@0
  1335
MAKE-ALL (Poly/ML) failed in ZF
clasohm@0
  1336
clasohm@0
  1337
ZF/sum/sumE2: deleted since unused
clasohm@0
  1338
ZF/sum/sum_iff,sum_subset_iff,sum_equal_iff: new
clasohm@0
  1339
ZF/univ/Transset_Vfrom: new; used in proof of Transset_Vset
clasohm@0
  1340
clasohm@0
  1341
6 August
clasohm@0
  1342
clasohm@0
  1343
Pure/goals/prepare_proof: after "Additional hypotheses", now actually
clasohm@0
  1344
prints them!
clasohm@0
  1345
clasohm@0
  1346
ZF/ordinal/Transset_Union_family, Transset_Inter_family: renamed from
clasohm@0
  1347
Transset_Union, Transset_Inter
clasohm@0
  1348
clasohm@0
  1349
ZF/ordinal/Transset_Union: new 
clasohm@0
  1350
ZF/univ/pair_in_univ: renamed Pair_in_univ
clasohm@0
  1351
clasohm@0
  1352
ZF/mono/product_mono: generalized to Sigma_mono; changed uses in trancl, univ
clasohm@0
  1353
clasohm@0
  1354
ZF/lfp/lfp_Tarski,def_lfp_Tarski: renamed from Tarski,def_Tarski; changed
clasohm@0
  1355
uses in extend_ind.ML, nat.ML, trancl.ML.
clasohm@0
  1356
clasohm@0
  1357
ZF/ex/misc: Schroeder-Bernstein Theorem moved here from lfp.ML
clasohm@0
  1358
clasohm@0
  1359
ZF/fixedpt.thy,.ML: renamed from lfp.thy,.ML, and gfp added
clasohm@0
  1360
clasohm@0
  1361
9 August
clasohm@0
  1362
clasohm@0
  1363
ZF/zf.thy/ndependent_tr,dependent_tr': deleted, since they are now on
clasohm@0
  1364
Syntax/sextension. 
clasohm@0
  1365
clasohm@0
  1366
11 August
clasohm@0
  1367
clasohm@0
  1368
Pure/library.ML: added functions
clasohm@0
  1369
assocs: (''a * 'b list) list -> ''a -> 'b list
clasohm@0
  1370
transitive_closure: (''a * ''a list) list -> (''a * ''a list) list
clasohm@0
  1371
clasohm@0
  1372
Pure/type.ML: deleted (inefficient) transitive_closure