2006-04-06 haftmann 2006-04-06 cleanup in datatype package
2006-04-06 haftmann 2006-04-06 small type annotation fix
2006-04-06 haftmann 2006-04-06 added hook for codegen_theorems.ML
2006-04-06 haftmann 2006-04-06 adaptions to change in typedef_package.ML
2006-04-06 haftmann 2006-04-06 added functions for definitional code generation
2006-04-06 haftmann 2006-04-06 added definitional code generator module: codegen_theorems.ML
2006-04-06 haftmann 2006-04-06 minor changes
2006-04-06 haftmann 2006-04-06 exported specification names
2006-04-05 haftmann 2006-04-05 minor extensions
2006-04-05 paulson 2006-04-05 pool of constants; definition expansion; current best settings
2006-03-31 paulson 2006-03-31 removed some illegal characters: they were crashing SML/NJ
2006-03-31 paulson 2006-03-31 Removal of unused code
2006-03-28 paulson 2006-03-28 Simplified version of Jia's filter. Now all constants are pooled, rather than relevance being compared against separate clauses. Rejects are no longer noted, and units cannot be added at the end.
2006-03-28 schirmer 2006-03-28 renamed map_val to map_ran
2006-03-28 schirmer 2006-03-28 added map_val, superseding map_at and substitute ----------------------------------------------------------------------
2006-03-28 haftmann 2006-03-28 some internal cleanup
2006-03-27 paulson 2006-03-27 removed illegal character codes
2006-03-26 urbanc 2006-03-26 simplified the proof at_fin_set_supp
2006-03-25 nipkow 2006-03-25 changed abbreviation for "infinite" back to translation because something didn't work during (output).
2006-03-24 huffman 2006-03-24 lazy patterns in lambda abstractions
2006-03-24 urbanc 2006-03-24 changed the it_prm proof to work for recursion
2006-03-24 urbanc 2006-03-24 tuned some proofs
2006-03-24 berghofe 2006-03-24 Removed occurrences of makestring, which does not exist in SML/NJ.
2006-03-23 nipkow 2006-03-23 Converted translations to abbbreviations. Removed a few odd functions from Map and AssocList. Moved chg_map from Map to Bali/Basis.
2006-03-23 berghofe 2006-03-23 Replaced iteration combinator by recursion combinator.
2006-03-23 paulson 2006-03-23 detection of definitions of relevant constants
2006-03-23 mengj 2006-03-23 Only display atpset theorems if Output.show_debug_msgs is true.
2006-03-22 urbanc 2006-03-22 added the first two simple proofs of the recursion combinator
2006-03-22 webertj 2006-03-22 comment fixed
2006-03-22 paulson 2006-03-22 Introduction of "whitelist": theorems forced past the relevance filter
2006-03-22 paulson 2006-03-22 Slight simplification of proofs
2006-03-22 paulson 2006-03-22 Removal of obsolete strategies. Initial support for locales: Frees and Consts treated similarly.
2006-03-22 webertj 2006-03-22 comment for conjI added
2006-03-22 nipkow 2006-03-22 translations -> abbreviations (a cool feature)
2006-03-21 wenzelm 2006-03-21 fixed example;
2006-03-21 wenzelm 2006-03-21 mark_boundT: produce well-typed term;
2006-03-21 wenzelm 2006-03-21 subtract (op =); pretty_proof: no abbrevs;
2006-03-21 wenzelm 2006-03-21 avoid polymorphic equality; tuned;
2006-03-21 wenzelm 2006-03-21 avoid polymorphic equality; subtract (op =);
2006-03-21 wenzelm 2006-03-21 moved gen_eq_set to library.ML;
2006-03-21 wenzelm 2006-03-21 added ~$$ (negative literal); combinators: avoid code duplication; tuned extend_lexicon;
2006-03-21 wenzelm 2006-03-21 avoid polymorphic equality;
2006-03-21 wenzelm 2006-03-21 remove (op =); tuned;
2006-03-21 wenzelm 2006-03-21 gen_eq_set, remove (op =);
2006-03-21 wenzelm 2006-03-21 abbreviation upto, length;
2006-03-21 wenzelm 2006-03-21 added subtract; tuned;
2006-03-21 wenzelm 2006-03-21 subtract (op =);
2006-03-21 wenzelm 2006-03-21 remove (op =);
2006-03-21 paulson 2006-03-21 Now SML/NJ-friendly (IntInf)
2006-03-21 paulson 2006-03-21 Removal of unnecessary simprules: simproc cancel_numerals now works without add_Suc, while the reason for the horrible isolateSuc is not known.
2006-03-20 wenzelm 2006-03-20 interpret: Proof.assert_forward_or_chain;
2006-03-20 paulson 2006-03-20 subsetI is often necessary
2006-03-20 paulson 2006-03-20 Now the setup for cancel_numerals accepts mixed Sucs/+ where the Sucs no longer need to be outermost.
2006-03-20 ballarin 2006-03-20 Tuned signature of Locale.add_locale(_i).
2006-03-18 wenzelm 2006-03-18 simplified mg_domain (use Sign.classes/arities_of); removed unused lift_local_theory_yield;
2006-03-18 wenzelm 2006-03-18 made $$ and "this" monomorphic (string);
2006-03-18 wenzelm 2006-03-18 tuned;
2006-03-18 wenzelm 2006-03-18 export arities_of instead of classes_arities_of;
2006-03-18 wenzelm 2006-03-18 updated;
2006-03-18 wenzelm 2006-03-18 renamed const less to lt;