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.
1995-12-22 paulson 1995-12-22 "prep_const" now calls compress_type to ensure sharing among types of constants in theories.
1995-12-22 paulson 1995-12-22 "prepare_proof" has been simplified because rewrite_rule and rewrite_goals_rule check for empty lists. The list of premises is *not* passed to Thm.compress; this was tried, but the potential storage gains seemed not to justify the cpu time required.
1995-12-22 paulson 1995-12-22 Now "standard" compresses theorems (for sharing). Also, rewrite_rule and rewrite_goals_rule check for the empty list of rewrites and do nothing in that case.
1995-12-22 paulson 1995-12-22 Now loads symtab.ML before term.ML. Functor > SymtabFun has been changed to the structure Symtab.
1995-12-20 regensbu 1995-12-20 changed predicate flat to is_flat in theory Fix.thy
1995-12-18 clasohm 1995-12-18 setting base_path is now optional
1995-12-18 clasohm 1995-12-18 added automatic handling of wrongly set base_path
1995-12-18 clasohm 1995-12-18 added subdir_of
1995-12-15 clasohm 1995-12-15 added chmod and chgrp
1995-12-15 clasohm 1995-12-15 init_html now makes sure that base_path contains a physical path and no symbolic links
1995-12-14 paulson 1995-12-14 Added Pelletier's problem 62, as corrected in AAR Newletter #31
1995-12-13 clasohm 1995-12-13 renamed parents_of to parents_of_name to avoid name clash with function from thm.ML
1995-12-11 nipkow 1995-12-11 layout
1995-12-09 clasohm 1995-12-09 removed quotes from consts and syntax sections
1995-12-08 nipkow 1995-12-08 Introduced Monad syntax Pat := Val; Cont
1995-12-08 paulson 1995-12-08 trivial, automatic changes
1995-12-08 nipkow 1995-12-08 Changed div_termination -> diff_less Corrected if_...
1995-12-08 paulson 1995-12-08 Improved error message, suggesting addition of type constraints if occurrences of the recursive set remain in the fixedpoint definition.
1995-12-08 paulson 1995-12-08 Now def of apfst uses pattern-matching
1995-12-08 paulson 1995-12-08 improved indentation
1995-12-08 paulson 1995-12-08 New function read_cterms is a combination of read_def_cterm and read_cterm. It reads and simultaneously type-checks a list of strings. cterm_of no longer catches exception TYPE; instead it must be caught later on and a message printed using Sign.exn_type_msg. More informative messages can be printed this way.
1995-12-08 paulson 1995-12-08 exports exn_type_msg for error messages. Calls new infer_types. Improved comments.
1995-12-08 paulson 1995-12-08 infer_types now takes a term list and a type list as argument. It is defined using the new function infer_terms. Error messages and comments also improved.
1995-12-08 paulson 1995-12-08 type_of1: improved error messages
1995-12-08 paulson 1995-12-08 Commented and renamed vars in readtm
1995-12-07 clasohm 1995-12-07 removed quotes from consts and syntax sections