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
lcp [Mon, 31 Oct 1994 15:41:20 +0100] rev 661
added final newline
lcp [Mon, 31 Oct 1994 15:35:43 +0100] rev 660
added header files; deleted commented-out code
nipkow [Fri, 28 Oct 1994 10:13:16 +0100] rev 659
Prepared the code for preservation of bound var names during rewriting. Still
requires a matching function for HO-patterns.
nipkow [Wed, 26 Oct 1994 17:41:40 +0100] rev 658
removed superfluous type_intrs in datatype com.
nipkow [Wed, 26 Oct 1994 15:20:55 +0100] rev 657
simplified syntax of infix continuous functiuons
wenzelm [Tue, 25 Oct 1994 13:16:49 +0100] rev 656
strip_quotes now exported;
wenzelm [Tue, 25 Oct 1994 13:15:34 +0100] rev 655
minor change of occs_const in dest_defn;
wenzelm [Tue, 25 Oct 1994 13:13:52 +0100] rev 654
added require_thy;
lcp [Mon, 24 Oct 1994 10:34:28 +0100] rev 653
HOL,ZF/IMP/Com.thy: tightening precedences to eliminate syntactic ambiguities.
constructor ";" now yields a low precedence; the reduction relations are
now more like infixes.