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