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
1995-12-07 clasohm 1995-12-07 removed quotes from consts and syntax sections
1995-12-07 clasohm 1995-12-07 removed quotes from syntax and consts sections
1995-12-06 clasohm 1995-12-06 fixed bug: cur_thyname was overwritten because of early assignment
1995-12-01 clasohm 1995-12-01 changed typeDecl
1995-12-01 clasohm 1995-12-01 removed quotes from types section
1995-12-01 clasohm 1995-12-01 added const_type to type_decl
1995-12-01 clasohm 1995-12-01 corrected diagrams for type and simpleType
1995-12-01 clasohm 1995-12-01 removed some more quotes
1995-12-01 clasohm 1995-12-01 changed HTML documentation
1995-12-01 clasohm 1995-12-01 modified simpleType
1995-12-01 clasohm 1995-12-01 removed debugging message; link to non-existing super index is now omitted silently
1995-12-01 clasohm 1995-12-01 simplified parser for constType
1995-12-01 clasohm 1995-12-01 removed quotes from consts and syntax sections
1995-11-30 clasohm 1995-11-30 removed spaghetti diagrams for constType
1995-11-29 clasohm 1995-11-29 removed quotes from consts and syntax sections
1995-11-29 clasohm 1995-11-29 changed syntax diagrams according to quote-less consts and syntax section
1995-11-29 clasohm 1995-11-29 added \label{sec:shell-scripts}
1995-11-29 clasohm 1995-11-29 added type class to simple_type