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