1996-02-05 clasohm 1996-02-05 expanded tabs
1996-02-05 clasohm 1996-02-05 expanded tabs
1996-02-02 clasohm 1996-02-02 renamed subtype.ML to typedef.ML
1996-02-01 nipkow 1996-02-01 documented split_all_tac in HOL.
1996-02-01 clasohm 1996-02-01 renamed subtype.ML to typedef.ML
1996-02-01 clasohm 1996-02-01 fixed two little bugs
1996-01-31 nipkow 1996-01-31 right-hard -> right-hand
1996-01-31 nipkow 1996-01-31 Typo
1996-01-30 clasohm 1996-01-30 fixed typo
1996-01-30 clasohm 1996-01-30 expanded tabs
1996-01-30 clasohm 1996-01-30 expanded tabs; removed commit() from ROOT.ML
1996-01-30 clasohm 1996-01-30 expanded tabs
1996-01-30 clasohm 1996-01-30 fixed typo
1996-01-30 clasohm 1996-01-30 expanded tabs
1996-01-29 clasohm 1996-01-29 inserted tabs again
1996-01-29 clasohm 1996-01-29 expanded tabs
1996-01-29 clasohm 1996-01-29 removed tabs
1996-01-29 clasohm 1996-01-29 added facility to associate arbitrary data with theories
1996-01-29 clasohm 1996-01-29 added absolute_path
1996-01-29 clasohm 1996-01-29 changed the way simpsets and information about datatypes are stored
1996-01-26 nipkow 1996-01-26 Streamlined defs in Relation and added new intro/elim rules to do with pattern matching in sets: {(x,y). ...} and UN (x,y):A. ...
1996-01-26 clasohm 1996-01-26 extended warning regarding MAKE_HTML databases
1996-01-26 clasohm 1996-01-26 added warning for databases made with set MAKE_HTML
1996-01-23 nipkow 1996-01-23 Added vcwp
1996-01-23 paulson 1996-01-23 Renamed letI to LetI (for consistency)
1996-01-23 paulson 1996-01-23 Added discussion of "let" and pattern-matching
1996-01-23 paulson 1996-01-23 Stylistic changes to discussion of pattern-matching
1996-01-23 nipkow 1996-01-23 Added a verified verification-condition generator.
1996-01-20 paulson 1996-01-20 Ran expandshort
1996-01-19 paulson 1996-01-19 Now expands TABS as well
1996-01-18 paulson 1996-01-18 trivial updates Isabelle94-5
1996-01-18 paulson 1996-01-18 New version number
1996-01-15 wenzelm 1996-01-15 *** empty log message ***
1996-01-15 wenzelm 1996-01-15 added Lattice demo;
1996-01-15 wenzelm 1996-01-15 added this stuff;
1996-01-15 wenzelm 1996-01-15 improved printing of errors in 'defs'; fixed small bug in 'standard' (it used to fail stripping shyps in some cases);
1996-01-15 clasohm 1996-01-15 added comments
1996-01-15 clasohm 1996-01-15 beautified file_info a bit
1996-01-15 clasohm 1996-01-15 fixed bug in file_info
1996-01-11 nipkow 1996-01-11 Removed bug in type unification. Negative indexes are not used any longer. Had to change interface to Type.unify to pass maxidx. Thus changes in the clients.
1996-01-09 clasohm 1996-01-09 simplified file_info by using System.filedate
1996-01-06 nipkow 1996-01-06 removed reference to Nat thms in elim_rls.
1996-01-06 nipkow 1996-01-06 Minor mod.
1996-01-02 nipkow 1996-01-02 Polished proofs.
1996-01-02 paulson 1996-01-02 Improving space efficiency of inductive/datatype definitions. Reduce usage of "open" and change struct open X; D end to let open X in struct D end end whenever possible -- removes X from the final structure. Especially needed for functors Intr_elim and Indrule.
1996-01-01 nipkow 1996-01-01 Modified non-empty-types warning in HOL.
1995-12-28 paulson 1995-12-28 Reduced indentation; no change in function
1995-12-28 paulson 1995-12-28 Purely cosmetic changes
1995-12-28 paulson 1995-12-28 Updated comments for compression functions
1995-12-28 paulson 1995-12-28 Removed unfold:thm from signature INTR_ELIM and from the functor result. It is never used outside, is easily recovered using bnd_mono and def_lfp_Tarski, and takes up considerable store.
1995-12-28 paulson 1995-12-28 Now mutual_induct is simply "True" unless it is going to be significantly different from induct -- either because there is mutual recursion or because it involves tuples.
1995-12-28 paulson 1995-12-28 fixed indentation
1995-12-23 nipkow 1995-12-23 New version of type sections and many small changes.
1995-12-22 paulson 1995-12-22 Note that unfold is not exported, that mutual_induct can be omitted (as the trivial theorem True), and comments on storage Also uses Datatype instead of Univ/Quniv as parent theory for lists, and omits quotes around types in theory files.
1995-12-22 paulson 1995-12-22 Added line breaks and other cosmetic changes
1995-12-22 nipkow 1995-12-22 defined take/drop by induction over list rather than nat.
1995-12-22 paulson 1995-12-22 Improving space efficiency of inductive/datatype definitions. Reduce usage of "open" and change struct open X; D end to let open X in struct D end end whenever possible -- removes X from the final structure. Especially needed for functors Intr_elim and Indrule. intr_elim.ML and constructor.ML now use a common Su.free_SEs instead of generating a new one. Inductive defs no longer export sumprod_free_SEs ZF/intr_elim: Removed unfold:thm from signature INTR_ELIM. It is never used outside, is easily recovered using bnd_mono and def_lfp_Tarski, and takes up considerable store. Moved raw_induct and rec_names to separate signature INTR_ELIM_AUX, for items no longer exported. mutual_induct is simply "True" unless it is going to be significantly different from induct -- either because there is mutual recursion or because it involves tuples.
1995-12-22 paulson 1995-12-22 Addition of compression, that is, sharing. Uses refs and Symtab (binary search trees) to get reasonable speed. Types and terms can be compressed.
1995-12-22 paulson 1995-12-22 Commented the datatype declaration of thm. Declared compress: thm -> thm to copy a thm and maximize sharing in it. "ext_axms" now calls Term.compress_term so that stored axioms use sharing.
1995-12-22 paulson 1995-12-22 Removed obsolete alist_of and st_of_alist. Is now simply a structure instead of a functor.