1997-06-06 paulson 1997-06-06 New example theory: Recdef
1997-06-05 nipkow 1997-06-05 added finite_converse
1997-06-05 nipkow 1997-06-05 Moved image_is_empty from Finite.ML to equalities.ML
1997-06-05 nipkow 1997-06-05 Modified a few defs and proofs because of the changes to theory Finite.thy.
1997-06-05 nipkow 1997-06-05 Finite.ML Finite.thy: Replaced `finite subset of' by mere `finite'. Relation.ML Trancl.ML: more thms WF.ML WF.thy: added `acyclic' WF_Rel.ML: moved some thms back into WF and added some new ones.
1997-06-05 paulson 1997-06-05 New recdef examples
1997-06-05 paulson 1997-06-05 Removal of freeze_vars and thaw_vars. New freeze_thaw
1997-06-05 paulson 1997-06-05 freezeT now refers to Type.freeze_thaw
1997-06-05 paulson 1997-06-05 Tidying of signature. More robust renaming in freeze_thaw. New tactic distinct_subgoals_tac
1997-06-05 paulson 1997-06-05 Removal of freeze_vars and thaw_vars (quite unused...)
1997-06-05 paulson 1997-06-05 Removal of radixstring from string_of_int; addition of string_of_indexname
1997-06-05 paulson 1997-06-05 There was never need for another copy of radixstring...
1997-06-05 paulson 1997-06-05 Numerous simplifications and removal of HOL-isms Addition of the "simpset" feature (replacing references to \!simpset)
1997-06-05 paulson 1997-06-05 Now loads theory Recdef
1997-06-05 paulson 1997-06-05 A slight simplification of optstring The new "simpset" keyword in the "recdef" declaration
1997-06-05 paulson 1997-06-05 Now extracts the predicate variable from induct0 insteead of trying to predict its name. The new "freeze" function requires this.
1997-06-05 paulson 1997-06-05 Deleted the obsolete "pred_list" relation
1997-06-05 paulson 1997-06-05 Documented the new distinct_subgoals_tac
1997-06-05 paulson 1997-06-05 A slight simplification of optstring
1997-06-05 paulson 1997-06-05 Now extracts the predicate variable from induct0 insteead of trying to predict its name
1997-06-05 paulson 1997-06-05 Made the pseudo-type of split_rule_var a separate argument
1997-06-04 wenzelm 1997-06-04 eliminated non-ASCII;
1997-06-04 wenzelm 1997-06-04 eliminated freeze_vars;
1997-06-04 mueller 1997-06-04 changed priority of -> from [6,5]5 to [1,0]0
1997-06-03 wenzelm 1997-06-03 is_blank: fixed space2;
1997-06-03 paulson 1997-06-03 No longer refers to internal TFL structures
1997-06-03 paulson 1997-06-03 More de-HOLification: using Free, Const, etc. instead of mk_var, mk_const Changed the TFL functor to a structure (currently called Prim)
1997-06-03 paulson 1997-06-03 New theory "Power" of exponentiation (and binomial coefficients)
1997-06-03 paulson 1997-06-03 New theorem about the cardinality of the powerset (uses exponentiation)
1997-06-02 paulson 1997-06-02 Type inference makes a Const here, perhaps elsewhere?thry.sml
1997-06-02 paulson 1997-06-02 poly_tvars allows recdefs to be made without type constraints
1997-06-02 paulson 1997-06-02 Corrected banner: it is W0, not MiniML
1997-06-02 paulson 1997-06-02 New statement and proof of free_tv_subst_var in order to cope with new rewrite rules Un_insert_left, Un_insert_right
1997-06-02 paulson 1997-06-02 Now Un_insert_left, Un_insert_right are default rewrite rules
1997-06-02 paulson 1997-06-02 Corrected statement of filter_append; added filter_size
1997-06-02 paulson 1997-06-02 Simplified proof
1997-06-02 paulson 1997-06-02 New theorems le_add_diff_inverse, le_add_diff_inverse2
1997-05-30 mueller 1997-05-30 trivial changes to incorporate CTL.thy and Example.ML in html file;
1997-05-30 paulson 1997-05-30 Simplified the calling sequence of CONTEXT_REWRITE_RULE Eliminated get_rhs, which was calling dest_Trueprop too many times
1997-05-30 paulson 1997-05-30 Moved "less_eq" to NatDef from Arith
1997-05-30 paulson 1997-05-30 New results including the basis for unique factorization
1997-05-30 paulson 1997-05-30 Now "primes" is a set
1997-05-30 paulson 1997-05-30 Now Divides must be the parent
1997-05-30 paulson 1997-05-30 New proofs about cardinality. Suggested by Florian Kammueller
1997-05-30 paulson 1997-05-30 Addition of Finite as parent allows cardinality theorems
1997-05-30 paulson 1997-05-30 Replacement of "divides" by "dvd" from Divides.thy, and updating of proofs
1997-05-30 paulson 1997-05-30 Overloading of "^" requires a type constraint
1997-05-30 paulson 1997-05-30 Overloading of "^" requires new type class "power", with types "nat" and "set" in that class. The operator itself is declared in Nat.thy
1997-05-30 paulson 1997-05-30 New theory Divides
1997-05-30 paulson 1997-05-30 Many new theorems about cardinality
1997-05-30 paulson 1997-05-30 Now Divides must be the parent
1997-05-30 paulson 1997-05-30 Moving div and mod from Arith to Divides Moving dvd from ex/Primes to Divides
1997-05-30 paulson 1997-05-30 flushOut ensures that no recent error message are lost (not certain this is necessary)
1997-05-27 wenzelm 1997-05-27 polyml-3.1 default again (for local work);
1997-05-27 wenzelm 1997-05-27 fixed -P (checkout only);
1997-05-27 wenzelm 1997-05-27 NJ 1.09.2x as factory default! Isabelle94-8
1997-05-27 mueller 1997-05-27 Last changes for new release 94-8
1997-05-27 wenzelm 1997-05-27 added 1.09.28 note;
1997-05-27 paulson 1997-05-27 New theorems suggested by Florian Kammueller
1997-05-27 paulson 1997-05-27 Restoration of the two "bypassed" theorems Union_quotient and quotient_disj