1994-01-18 lcp 1994-01-18 Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated functions from sign.ML to thm.ML or drule.ML. This allows the "prop" field of a theorem to be regarded as a cterm -- avoids expensive calls to cterm_of.
1994-01-18 nipkow 1994-01-18 some optimizations of Larry's
1994-01-14 lcp 1994-01-14 corrected comments
1994-01-14 lcp 1994-01-14 corrected comments
1994-01-14 nipkow 1994-01-14 optimized net for matching of abstractions to speed up simplifier
1994-01-11 nipkow 1994-01-11 moved misplaced comment
1994-01-11 wenzelm 1994-01-11 removed Syntax/parse_tree.ML;
1994-01-11 nipkow 1994-01-11 optimized the number of eta-contractions in rewriting
1994-01-10 clasohm 1994-01-10 added a check for existence of a temporary file before removing it
1994-01-10 clasohm 1994-01-10 used unlink for delete_files instead of calling rm
1994-01-10 wenzelm 1994-01-10 commented out sig constraint of functor (for debugging purposes);
1994-01-07 lcp 1994-01-07 ZF/perm/image_comp: new
1994-01-05 nipkow 1994-01-05 got rid of METAHYPS due to the change of the basic simplification routines (see update of Pure/{thm,drule,tactic}.ML)
1994-01-05 nipkow 1994-01-05 adapted a proof to the new solver (see change of FOL/simpdata.ML)
1994-01-05 nipkow 1994-01-05 updated solver of FOL_ss. see change of HOL/simpdata.ML
1994-01-05 nipkow 1994-01-05 added new parameter to the simplification tactics which indicates if assumptions are to be simplified and/or to be used when simplifying the conclusion. This gets rid of METAHYPS and speeds up simplification of goals with big assumptions.
1994-01-05 nipkow 1994-01-05 added lexical class of type variables
1994-01-05 nipkow 1994-01-05 shortened msg
1994-01-04 nipkow 1994-01-04 added fake_cterm_of to speed up rewriting
1994-01-04 wenzelm 1994-01-04 commented out sig constraint of functor (for debugging purposes);
1994-01-04 nipkow 1994-01-04 changed tracing of simplifier
1994-01-02 nipkow 1994-01-02 optimized simplifier - signature of rewritten term stays constant
1993-12-30 clasohm 1993-12-30 added "Reading thy-File" message
1993-12-30 nipkow 1993-12-30 added subsig: sg * sg -> bool to test if one signature is contained in another.
1993-12-29 wenzelm 1993-12-29 added sys_error;
1993-12-22 clasohm 1993-12-22 fixed a bug in update/next_level which occured when a child wasn't loaded
1993-12-21 nipkow 1993-12-21 added empty type-abbr field to extend_theory
1993-12-21 nipkow 1993-12-21 added []-field to extend_theory: no type abbreviations.
1993-12-21 nipkow 1993-12-21 Added []-field to extend_theory to accomodate type abbreviations.
1993-12-21 nipkow 1993-12-21 Necessary changes to accomodate type abbreviations.
1993-12-21 wenzelm 1993-12-21 pretty_thm is now exported;
1993-12-21 lcp 1993-12-21 new section for equality properties
1993-12-14 nipkow 1993-12-14 Updated read_insts to approximate simultaneous type checking of substitution pairs.
1993-12-13 lcp 1993-12-13 added isabelle-users paragraph
1993-12-13 lcp 1993-12-13 added mention of simplifier, splitter, hypsubst
1993-12-13 lcp 1993-12-13 new year
1993-12-10 nipkow 1993-12-10 updated instantiate to deal with type clashes
1993-12-10 lcp 1993-12-10 ZF/equalities/SUM_eq_UN: new ZF/equalities: corrected bound variable anomalies in some distributive laws
1993-12-10 lcp 1993-12-10 Pure/tactic/compose_inst_tac: when catching exception THM, prints the message before failing!! This reports the reason for failure in cases like by (res_inst_tac [("P", "?Q(a)")] mp 1); in which ?Q appears in mp with a different type.
1993-12-09 nipkow 1993-12-09 deleted harmful basify, which pulled rewrite rules down to base type. Not needed for new simplifier.
1993-12-06 nipkow 1993-12-06 added rep_tsig Isabelle93
1993-12-06 nipkow 1993-12-06 last minute changes, eg literal tokens -> delimiters and valued tokens -> names.
1993-12-06 lcp 1993-12-06 ZF/univ/in_Vfrom_limit: new ZF/univ/sum_in_Vfrom, etc: streamlined proofs using in_Vfrom_limit
1993-12-06 lcp 1993-12-06 ZF/ord/Ord_Un,Ord_Int,Un_upper1_le,Un_upper2_le: new
1993-12-06 nipkow 1993-12-06 Typos and style
1993-12-03 lcp 1993-12-03 Changed Acknowledgements
1993-12-03 lcp 1993-12-03 Acknowledged Carsten Clasohm
1993-12-03 lcp 1993-12-03 New distributive laws for Sigma and UN
1993-12-02 lcp 1993-12-02 removal of amssymbols.sty and lcp.sty; addition of iman.sty
1993-12-01 lcp 1993-12-01 ZF/ex/ROOT: changed many time_use calls to time_use_thy or else deleted them, to make the most of the load-path mechanism. (use_thy adds the new theory to the list of loaded theories.)
1993-12-01 lcp 1993-12-01 minor corrections
1993-12-01 lcp 1993-12-01 new references
1993-12-01 lcp 1993-12-01 now inspects FOLP_build_completed
1993-12-01 lcp 1993-12-01 now declares FOLP_build_completed
1993-11-30 wenzelm 1993-11-30 *** empty log message ***
1993-11-30 wenzelm 1993-11-30 *** empty log message ***
1993-11-30 lcp 1993-11-30 ZF/ex/llist_eq/lleq_Int_Vset_subset_lemma, ZF/ex/counit/counit2_Int_Vset_subset_lemma: now uses QPair_Int_Vset_subset_UN ZF/ex/llistfn/flip_llist_quniv_lemma: now uses transfinite induction and QPair_Int_Vset_subset_UN ZF/ex/llist/llist_quniv_lemma: now uses transfinite induction and QPair_Int_Vset_subset_UN
1993-11-30 wenzelm 1993-11-30 changed split_filename, remove_ext; added base_name;
1993-11-30 wenzelm 1993-11-30 *** empty log message ***
1993-11-30 lcp 1993-11-30 ZF/quniv/QPair_Int_Vset_subset_UN: new, isolates key argument of many coinduction proofs ZF/quniv: deleted the following obsolete theorems (saved on Isa/old): Int_Vfrom_0_in_quniv Pair_in_quniv_D QInl_Int_Vfrom_succ_in_quniv QInl_Int_quniv_in_quniv QPair_Int_Vfrom_in_quniv QPair_Int_Vfrom_succ_in_quniv QPair_Int_quniv_eq QPair_Int_quniv_in_quniv QPair_Int_quniv_in_quniv product_Int_quniv_eq quniv_Int_Vfrom zero_Int_in_quniv