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