lcp [Mon, 21 Nov 1994 11:49:36 +0100] rev 721
Pure/thm/norm_term_skip: new, for skipping normalization of the context
Pure/thm/bicompose_aux: now computes nlift (number of lifted assumptions in
new subgoals) and avoids normalizing the first nlift assumptions in the
case where the proof state is not affected.
Pure/thm/norm_term_skip: now normalizes types of parameters
Pure/thm/THM: aligned colons
lcp [Mon, 21 Nov 1994 11:33:23 +0100] rev 720
Pure/sequence: added comment explaining that memoing sequences were found
to be much slower (due to overheads) than the sequences currently used.
lcp [Mon, 21 Nov 1994 11:27:10 +0100] rev 719
Pure/envir/norm_term: replaced equality test for [] by null
lcp [Mon, 21 Nov 1994 10:51:40 +0100] rev 718
page 157 erratum
lcp [Mon, 21 Nov 1994 10:39:32 +0100] rev 717
now searches all subdirectories of object-logics
whether or not they are called "ex"
nipkow [Fri, 18 Nov 1994 13:14:23 +0100] rev 716
Chnaged simplifier description (lhss)
clasohm [Fri, 18 Nov 1994 13:08:10 +0100] rev 715
added call of store_theory after thy file has been read
nipkow [Fri, 18 Nov 1994 13:04:51 +0100] rev 714
Updated description of valid lhss.
lcp [Thu, 17 Nov 1994 22:01:08 +0100] rev 713
In ZF, type i has class term, not (just) logic
clasohm [Mon, 14 Nov 1994 14:47:20 +0100] rev 712
added check for newlines not enclosed by '\' inside strings
clasohm [Mon, 14 Nov 1994 14:29:20 +0100] rev 711
updated remarks about grammar; added section about ambiguities
wenzelm [Mon, 14 Nov 1994 11:57:32 +0100] rev 710
exported 'cat';
lcp [Mon, 14 Nov 1994 10:49:39 +0100] rev 709
Pure/tctical/select: now uses cprems_of instead of prems_of and cterm_of:
new SELECT_GOAL is MUCH faster
lcp [Mon, 14 Nov 1994 10:46:50 +0100] rev 708
Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
lcp [Mon, 14 Nov 1994 10:41:25 +0100] rev 707
Added month for Coens thesis
lcp [Fri, 11 Nov 1994 10:53:41 +0100] rev 706
removal of FOL_dup_cs
lcp [Fri, 11 Nov 1994 10:50:49 +0100] rev 705
removal of HOL_dup_cs
rotation of arguments in split, nat_case, sum_case, list_case
lcp [Fri, 11 Nov 1994 10:42:55 +0100] rev 704
Provers/hypsubst/REPEATN: deleted; using REPEAT_DETERM_N instead.
lcp [Fri, 11 Nov 1994 10:41:09 +0100] rev 703
Pure/tctical/REPEAT_DETERM_N,REPEAT_DETERM1,REPEAT_DETERM_FIRST,
REPEAT_DETERM_SOME: new
lcp [Fri, 11 Nov 1994 10:33:05 +0100] rev 702
FOL/intprover/safe_tac: now uses REPEAT_DETERM_FIRST instead of REPEAT_DETERM
lcp [Fri, 11 Nov 1994 10:31:51 +0100] rev 701
argument swaps in HOL
lcp [Thu, 10 Nov 1994 11:36:40 +0100] rev 700
HOL,ZF/Makefile: enclosed multiple "use" calls in parentheses. This
ensures that if one dies, all die. BUT NOT Pure/Makefile, where
PolyML.use"POLY" makes the identifier "use" visible.
lcp [Thu, 10 Nov 1994 11:06:44 +0100] rev 699
updated pathnames
lcp [Wed, 09 Nov 1994 15:47:11 +0100] rev 698
updated discussion of congruence rules in first section
clasohm [Wed, 09 Nov 1994 13:50:59 +0100] rev 697
changed warning for extremely ambiguous expressions
lcp [Thu, 03 Nov 1994 16:52:19 +0100] rev 696
Pure/goals/prepare_proof/mkresult: now smashes flexflex pairs in the final
result.
lcp [Thu, 03 Nov 1994 16:39:41 +0100] rev 695
ZF/ex/Ramsey,Rmap,misc.ML: modified for new definition of Pi(A,B)
lcp [Thu, 03 Nov 1994 16:05:22 +0100] rev 694
ZF/ex/Ramsey,Rmap,misc.ML: modified for new definition of Pi(A,B)
lcp [Thu, 03 Nov 1994 13:42:39 +0100] rev 693
ZF/Perm/inj_converse_fun: tidied; removed uses of PiI/E
ZF/Perm/comp_fun: tidied; removed use of PiI
lcp [Thu, 03 Nov 1994 12:43:42 +0100] rev 692
ZF/InfDatatype/fun_Vcsucc: removed use of PiE
lcp [Thu, 03 Nov 1994 12:39:39 +0100] rev 691
ZF/func: tidied many proofs, using new definition of Pi(A,B)
ZF/func/PiI,PiE: removed
ZF/func/Pi_iff_old: new
ZF/func/Pi_memberD: new; simpler, replaces memberPiE
lcp [Thu, 03 Nov 1994 12:35:41 +0100] rev 690
ZF: NEW DEFINITION OF PI(A,B)
Was Pi(A,B) == {f: Pow(Sigma(A,B)). ALL x:A. EX! y. <x,y>: f}
Now function(r) == ALL x y. <x,y>:r --> (ALL y'. <x,y'>:r --> y=y')
Pi(A,B) == {f: Pow(Sigma(A,B)). A<=domain(f) & function(f)}"
This simplifies many proofs, since (a) the top-level definition has fewer
bound variables (b) the "total" and "function" properties are separated
(c) the awkward EX! quantifier is eliminated.
ZF/ZF.thy/function: new definition
lcp [Thu, 03 Nov 1994 12:30:55 +0100] rev 689
ZF/Fixedpt/subset_cs: moved to ZF/subset.ML
lcp [Thu, 03 Nov 1994 12:26:59 +0100] rev 688
ZF/Fixedpt/subset0_cs: moved to ZF/ZF.ML
lcp [Thu, 03 Nov 1994 12:23:19 +0100] rev 687
ZF/domrange/converse_iff: new
lcp [Thu, 03 Nov 1994 12:06:37 +0100] rev 686
ZF/upair/theI2: new
lcp [Thu, 03 Nov 1994 11:58:16 +0100] rev 685
ZF/equalities/domain_converse,range_converse,
prod_Un_distrib2,prod_Int_distrib2: new
lcp [Thu, 03 Nov 1994 11:52:04 +0100] rev 684
ZF/Fixedpt/subset0_cs: moved to ZF/ZF.ML
ZF/Fixedpt/subset_cs: moved to ZF/subset.ML
lcp [Thu, 03 Nov 1994 11:45:41 +0100] rev 683
Cardinal_AC/surj_implies_inj: uses Pi_memberD instead of memberPiE
clasohm [Thu, 03 Nov 1994 08:34:53 +0100] rev 682
added warning message
"Currently parsed expression could be extremely ambiguous."
lcp [Wed, 02 Nov 1994 12:48:22 +0100] rev 681
Provers/classical: now takes theorem "classical" as argument, proves "swap"
Provers/classical/depth_tac,deepen_tac: new
lcp [Wed, 02 Nov 1994 12:44:03 +0100] rev 680
Provers/hypsubst: greatly simplified! No longer simulates a
"eres_inst_tac" using rev_cut_eq; instead simply rotates the chosen
equality to the end!
lcp [Wed, 02 Nov 1994 10:45:14 +0100] rev 679
Pure/sign/infer_types/exn_type_msg: new, for more uniform handling of
exception TYPE
nipkow [Wed, 02 Nov 1994 09:09:30 +0100] rev 678
Modified pattern.ML to perform proper matching of Higher-Order Patterns.
Modified thm.ML to preserve bound var names during rewriting.
Renamed eta_matches to matches.
lcp [Tue, 01 Nov 1994 10:40:10 +0100] rev 677
FOL/FOL/swap: deleted
FOL/FOL: tidied the signature
lcp [Tue, 01 Nov 1994 10:32:18 +0100] rev 676
HOLCF/Ssum3.ML: changed res_inst_tac [("P"... to res_inst_tac [("Pa" in
some very ugly proofs. Needed to handle new variable names in swap.
lcp [Mon, 31 Oct 1994 18:15:24 +0100] rev 675
ZF/ZF.thy: added precedences to @RepFun to disambiguate phrases like {x:A.x:B}
lcp [Mon, 31 Oct 1994 18:11:12 +0100] rev 674
ZF/domrange/image_subset: tidied
lcp [Mon, 31 Oct 1994 18:09:32 +0100] rev 673
ZF/upair/mem_asym,succ_inject: tidied
lcp [Mon, 31 Oct 1994 18:07:29 +0100] rev 672
com1,2: added simplifier calls to remove use of ssubst in fast_tac
lcp [Mon, 31 Oct 1994 18:03:14 +0100] rev 671
Pure/tctical/THEN_ELSE: new
lcp [Mon, 31 Oct 1994 18:01:02 +0100] rev 670
Pure/tactic/build_netpair: now takes two arguments
lcp [Mon, 31 Oct 1994 17:59:49 +0100] rev 669
Pure/sequence/hd,tl: new
lcp [Mon, 31 Oct 1994 17:55:43 +0100] rev 668
Pure/drule/thin_rl: new
lcp [Mon, 31 Oct 1994 17:14:42 +0100] rev 667
FOL/ex/ROOT: now loads mini.ML
lcp [Mon, 31 Oct 1994 17:09:10 +0100] rev 666
FOL/ROOT/FOL_dup_cs: removed as obsolete
FOL/ROOT: no longer proves rev_cut_eq for hyp_subst_tac
lcp [Mon, 31 Oct 1994 16:45:19 +0100] rev 665
FOL/ex/cla: proofs now use deepen_tac instead of best_tac FOL_dup_cs
lcp [Mon, 31 Oct 1994 16:39:20 +0100] rev 664
ZF/ZF/ex1_functional: moved to FOL/ROOT
lcp [Mon, 31 Oct 1994 15:49:58 +0100] rev 663
Miniscope conversoin; example of formula rewriting
lcp [Mon, 31 Oct 1994 15:45:54 +0100] rev 662
ZF/OrderArith/thin: deleted as obsolete
ZF/OrderArith/wf_on_radd: now uses thin_rl