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
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.
lcp [Fri, 21 Oct 1994 09:58:05 +0100] rev 652
ZF/intr_elim/elim_rls: now includes Pair_inject, since coinductive
definitions may involve ordinary pairs. (HOL/intr_elim does not require
this change)
lcp [Fri, 21 Oct 1994 09:53:38 +0100] rev 651
Pure/Unify/IMPROVING "CLEANING" OF FLEX-FLEX PAIRS: Old code would refuse
to simplfy %x y.?a(x) =?= %x y.?b(f(?c(y), y)) because it found the flexible
path to y before the rigid path. New code simplifies this to
%x.?a(x) =?= %x.?d, eliminating ?a.
Pure/Unify/rigid_bound: preliminary check for rigid paths to the banned
bound variables
Pure/Unify/change_bnos: any occurrences of the banned bound variables must
now be flexible, causing abandonment of the "cleaning"
lcp [Fri, 21 Oct 1994 09:51:01 +0100] rev 650
LK/hardquant/37: deleted call to flexflex_tac: no longer needed
lcp [Fri, 21 Oct 1994 09:47:02 +0100] rev 649
LCF/LCF.thy: the constant VOID had mixfix syntax "()" !! Added quotes.
lcp [Fri, 21 Oct 1994 09:35:24 +0100] rev 648
FOLP/IFOLP.thy: tightening precedences to eliminate syntactic ambiguities.
Now proof objects have high precedences. Eliminates ambiguity in a=b:P
being parsed as (a=b):P.
lcp [Wed, 19 Oct 1994 09:54:38 +0100] rev 647
ZF/Fixedpt/coinduct: modified proof to suppress deep unification
lcp [Wed, 19 Oct 1994 09:48:13 +0100] rev 646
new comments explaining abandoned change
lcp [Wed, 19 Oct 1994 09:44:31 +0100] rev 645
LCF/fix/lfp_is_FIX: modified proof to suppress deep unification
lcp [Wed, 19 Oct 1994 09:41:48 +0100] rev 644
FOL/ex/cla/58: slightly shorter proof
lcp [Wed, 19 Oct 1994 09:39:23 +0100] rev 643
trivial update to reference
lcp [Wed, 19 Oct 1994 09:23:56 +0100] rev 642
CCL/Gfp/coinduct2, coinduct3: modified proofs to suppress deep unification
CCL/CCL, Fix, Gfp, Hered, Set, Term, Trancl, Type, Wfd: expanded shorthands
wenzelm [Wed, 12 Oct 1994 16:38:58 +0100] rev 641
add_defs: improved error messages;
installed new print_goals with nice 'env mode';
wenzelm [Wed, 12 Oct 1994 16:34:52 +0100] rev 640
removed old comment;
wenzelm [Wed, 12 Oct 1994 16:34:00 +0100] rev 639
remove _explode, _implode and trfuns;
wenzelm [Wed, 12 Oct 1994 16:32:06 +0100] rev 638
prove_subclass, prove_arity now exported;
minor internal changes;
wenzelm [Wed, 12 Oct 1994 16:31:01 +0100] rev 637
added is_equals: term -> bool;
wenzelm [Wed, 12 Oct 1994 16:30:19 +0100] rev 636
type_args, opt_witness now exported;
added AxClass.;
wenzelm [Wed, 12 Oct 1994 16:29:10 +0100] rev 635
AxClass no longer open;
lcp [Wed, 12 Oct 1994 12:20:18 +0100] rev 634
{HOL,ZF}/intr_elim/intro_tacsf: now calls DEPTH_SOLVE_1 instead of REPEAT to
solve the goal fully
lcp [Wed, 12 Oct 1994 12:09:54 +0100] rev 633
{HOL,ZF}/indrule/ind_tac: now calls DEPTH_SOLVE_1 instead of REPEAT, to
solve the goal fully before proceeding
{HOL,ZF}/indrule/mutual_ind_tac: ensures that calls to "prem" cannot loop;
calls DEPTH_SOLVE_1 instead of REPEAT to solve the goal fully
wenzelm [Wed, 12 Oct 1994 11:09:11 +0100] rev 632
fixed infix names in print_translations;
lcp [Wed, 12 Oct 1994 09:48:32 +0100] rev 631
Pure/tctical/suppress_tracing: new; can now switch tracing off until the
next tactical call. There is no good way of doing this because of
backtracking.
Pure/tctical/exec_trace_command,tracify,traced_tac: these set, test and
reset suppress_tracing
lcp [Wed, 12 Oct 1994 09:42:32 +0100] rev 630
Minor reference updates
lcp [Wed, 12 Oct 1994 09:20:17 +0100] rev 629
Moving theory LList to ex directory
nipkow [Mon, 10 Oct 1994 18:09:58 +0100] rev 628
corrected problems with changed binding power of ::.
nipkow [Mon, 10 Oct 1994 12:57:23 +0100] rev 627
README file
clasohm [Sat, 08 Oct 1994 13:45:40 +0100] rev 626
changed precedences of _constrain (i.e. "::")
nipkow [Thu, 06 Oct 1994 18:40:18 +0100] rev 625
New version
clasohm [Tue, 04 Oct 1994 13:02:16 +0100] rev 624
made major changes to grammar;
added call of Type.infer_types to automatically eliminate ambiguities
clasohm [Tue, 04 Oct 1994 13:01:17 +0100] rev 623
added print_msg;
added call of Type.infer_types to resolve ambiguities
nipkow [Tue, 27 Sep 1994 14:23:46 +0100] rev 622
Modified termord to take account of the Abs-Abs case.
wenzelm [Mon, 26 Sep 1994 17:56:21 +0100] rev 621
improved expand_typ (now handles TVars);
slightly changed ext_tsig_abbrs;
added ext_tsig_arities;
removed extend_tsig;
various internal changes;
wenzelm [Mon, 26 Sep 1994 17:55:45 +0100] rev 620
exported pretty_sort;
various minor internal changes;
wenzelm [Mon, 26 Sep 1994 17:36:10 +0100] rev 619
added init_pps;
wenzelm [Mon, 26 Sep 1994 17:35:45 +0100] rev 618
added init_database (somewhat experimental);
wenzelm [Mon, 26 Sep 1994 17:35:23 +0100] rev 617
added flag show_no_free_types: bool ref;
wenzelm [Mon, 26 Sep 1994 17:34:59 +0100] rev 616
explode_tr now produces leadings 0s;
implode_ast_tr' now quotes result;
wenzelm [Wed, 21 Sep 1994 15:39:02 +0200] rev 615
minor cleanup, added 'syntax' section;
lcp [Thu, 15 Sep 1994 13:13:54 +0200] rev 614
now mentions that the sections are available as
Datatypes and (Co)Inductive Definitions in Isabelle/HOL
wenzelm [Wed, 14 Sep 1994 16:11:19 +0200] rev 613
removed lookup_const (use Sign.const_type instead);
wenzelm [Wed, 14 Sep 1994 16:05:39 +0200] rev 612
replaced lookup_const by Sign.const_type;
wenzelm [Wed, 14 Sep 1994 16:02:06 +0200] rev 611
now uses Sign.const_type;
wenzelm [Wed, 14 Sep 1994 14:49:56 +0200] rev 610
letrec syntax: replaced "id" by "idt";
lcp [Tue, 13 Sep 1994 11:39:49 +0200] rev 609
updated for Isabelle94
lcp [Tue, 13 Sep 1994 11:19:38 +0200] rev 608
now uses find to locate .thy.ML files everywhere
lcp [Tue, 13 Sep 1994 10:42:34 +0200] rev 607
updated the identifier "version"
lcp [Tue, 13 Sep 1994 10:26:24 +0200] rev 606
minor updates
lcp [Mon, 12 Sep 1994 13:20:07 +0200] rev 605
New Makefile for Logics Manual
lcp [Mon, 12 Sep 1994 13:06:07 +0200] rev 604
New Makefile for Reference Manual
lcp [Mon, 12 Sep 1994 13:01:38 +0200] rev 603
New Makefile for Introduction
lcp [Mon, 12 Sep 1994 12:45:10 +0200] rev 602
New Makefile for ind-defs
nipkow [Sun, 11 Sep 1994 12:52:00 +0200] rev 601
Added primrec section
nipkow [Sun, 11 Sep 1994 10:59:09 +0200] rev 600
Added primrec section.
lcp [Fri, 09 Sep 1994 13:10:09 +0200] rev 599
now in a format that could be published
lcp [Fri, 09 Sep 1994 12:34:54 +0200] rev 598
added Abrial and Laffitte; Kunen; Winskel, etc.
lcp [Fri, 09 Sep 1994 12:25:56 +0200] rev 597
Updated for existence of HOL version and infinitely
branching datatypes
lcp [Fri, 09 Sep 1994 11:57:49 +0200] rev 596
Per cent (%) now functions as comment character in tt
box environment
lcp [Fri, 09 Sep 1994 11:52:38 +0200] rev 595
Added mention of directory IMP; tidied the section on examples.