0

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 
MAKEALL (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 
MAKEALL (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 
MAKEALL (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 
MAKEALL (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 
MAKEALL (Poly/ML) ran perfectly. It took 2:50 hours.


113 


114 
Pure/Thy/scan/string: now correctly recognizes MLstyle strings.


115 


116 
15 February


117 


118 
MAKEALL (NJ 0.75) ran perfectly. It took 1:37 hours (on albatross)


119 
MAKEALL (NJ 0.75) ran perfectly. It took 2:42 hours (on dunlin)


120 
MAKEALL (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 
MAKEALL (NJ 0.75) ran perfectly. It took 3:37 hours


134 
MAKEALL (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 
MAKEALL (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 
MAKEALL (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 
MAKEALL (Poly/ML) ran perfectly.


189 


190 
18 March


191 


192 
MAKEALL (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 
MAKEALL (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; reorganized 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 overwriting


218 
the library functions fst, snd


219 


220 
HOL/fun/image_compose: new


221 


222 
21 March


223 


224 
MAKEALL (NJ 0.93) ran perfectly. It took 3:50 hours


225 
MAKEALL (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 overwriting


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 wellfounded 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 wellfounded 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 flexflex 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 
MAKEALL (NJ 0.93) ran perfectly. It took 4:25 hours!


294 
MAKEALL (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 nonStandard 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 
MAKEALL on this directory ran perfectly


310 
/usr/groups/theory/mlaftp/Isabelle92.tar.Z: replaced by new version


311 


312 
29 March


313 


314 
MAKEALL (NJ 0.93) ran perfectly. It took 4:14 hours!


315 
MAKEALL (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 
MAKEALL (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 
MAKEALL (NJ 0.93) ran perfectly. It took 4:05 hours!


349 
MAKEALL (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 
MAKEALL (NJ 0.93) ran perfectly. It took 4:03 hours!


415 
MAKEALL (Poly/ML) ran perfectly. It took 3:28 hours!


416 


417 
FOLP/{intprover,classical}/safe_step_tac: uses eq_assume_tac, not assume_tac


418 
FOLP/{intprover,classical}/inst_step_tac: restored, calls assume and mp_tac


419 
FOLP/{intprover,classical}/step_tac: calls inst_step_tac


420 


421 
{FOL,FOLP}/intprover/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/{intprover,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 
MAKEALL (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 flexflex 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 
MAKEALL (Poly/ML) failed in HOL (ASM_SIMP_TAC redefined!) and LK


447 


448 
LK/ex/hardquant/37: added "by flexflex_tac" to compensate for flexflex


449 
changes


450 


451 
Pure/goals/gethyps: now calls METAHYPS directly


452 


453 
rmlogfiles: 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 
MAKEALL (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/proplog/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/proplog/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 
MAKEALL (NJ 0.93) ran perfectly. It took 3:39 hours (4 mins faster)


503 
MAKEALL (Poly/ML) ran perfectly. It took 3:23 hours (5 mins faster)


504 


505 
ZF/simpdata/ZF_ss: deleted anti_refl_rew; nonlinear 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 objectlogics.


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 
MAKEALL (NJ 0.93) failed in HOL due to lack of disc space.


531 
MAKEALL (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 
MAKEALL 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 
MAKEALL (NJ 0.93) ran perfectly. It took 3:44 hours


563 
MAKEALL (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 
makeall: now compresses the log files, which were taking up 4M; this


568 
reduces their space by more than 1/3


569 


570 
rmlogfiles: 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 
MAKEALL (NJ 0.93) ran perfectly. It took 3:52 hours??


583 
MAKEALL (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 
MAKEALL (NJ 0.93) ran out of space in LK.


599 
MAKEALL (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 
writeprotected


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 
MAKEALL (Poly/ML) ran perfectly. It took 3:18 hours


615 


616 
** Installation of new HOL from Tobias **


617 


618 
HOL/ex/{finite,proplog} 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 
MAKEALL (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 
MAKEALL (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/lexprod: 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 
MAKEALL (NJ 0.93) ran out of space in HOL.


674 
MAKEALL (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 
MAKEALL (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 
MAKEALL (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 
MAKEALL (Poly/ML) ran perfectly. It took 3:39 hours


745 


746 
**** New tar file 92.tar.z placed on /homes/lcp (376K) ****


747 


748 
MAKEALL (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 nonwriteable area.


760 


761 
HOL/arith: renamed / and // to div and mod


762 
ZF/arith: renamed #/ and #// to div and mod


763 


764 
MAKEALL (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 
makeall: 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 
MAKEALL (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 objectlogic 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 
MAKEALL (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 
MAKEALL (Poly/ML) ran perfectly. It took 2:07 hours on albatross.


803 
MAKEALL (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 
MAKEALL (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 bottomup 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 
(* bottomup 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 
metathms 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 objectlogic


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 
MAKEALL (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 
MAKEALL (Poly/ML) ran perfectly. It took 2:23 hours on albatross (with CCL)


960 


961 
MAKEALL (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 
MAKEALL (Poly/ML) ran perfectly. It took 2:23 hours on albatross.


971 
MAKEALL (NJ 0.93) failed in HOL due to lack of ".ML" extension


972 


973 
HOL/fun/rangeE,imageE: etaexpanded 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: coinduction rules applied with res_inst_tac to state the


983 
bisimulation directly


984 


985 
2 July


986 


987 
MAKEALL (NJ 0.93) ran perfectly. It took 2:10 hours on albatross.


988 
MAKEALL (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 
29Jun1993 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 
30Jun1993 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 
30Jun1993, 05Jul1993 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 
01Jul1993 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 
MAKEALL (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 
MAKEALL (NJ 0.93) ran perfectly. It took 2:13 hours on albatross.


1148 
MAKEALL (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 listfn.thy, listfn.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 btfn.thy, btfn.ML


1182 
ZF/ex/bt.ML: new version simply holds the datatype definition


1183 


1184 
ZF/ex/term.thy,term.ML: files renamed termfn.thy, termfn.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 
MAKEALL (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 
MAKEALL (NJ 0.93) failed in ZF due to Compiler bug: elabDecl:open:FctBodyStr


1312 
MAKEALL (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 
MAKEALL (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: SchroederBernstein 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
