2006-04-08 wenzelm 2006-04-08 refined 'abbreviation';
2006-04-08 haftmann 2006-04-08 made symlink relative
2006-04-08 haftmann 2006-04-08 made symlink relative
2006-04-08 kleing 2006-04-08 converted Müller to Mueller to make smlnj 110.58 work
2006-04-07 berghofe 2006-04-07 Fixed bug that caused proof of induction rule to fail for inductive sets with trivial introduction rules such as "x : S ==> x : S".
2006-04-07 kleing 2006-04-07 remame ASeries to Arithmetic_Series
2006-04-07 berghofe 2006-04-07 Added alternative version of thms_of_proof that does not recursively descend into proofs of (named) theorems.
2006-04-07 mengj 2006-04-07 hash table now stores thm and get_clasimp_atp_lemmas returns thm rather than term.
2006-04-07 mengj 2006-04-07 filter now accepts axioms as thm, instead of term.
2006-04-07 mengj 2006-04-07 tptp_write_file accepts axioms as thm.
2006-04-07 mengj 2006-04-07 added another function for CNF.
2006-04-07 mengj 2006-04-07 lemmas returned from ResClasimp.get_clasimp_atp_lemmas are thm rather than term.
2006-04-07 kleing 2006-04-07 renamed ASeries to Arithmetic_Series, removed the ^M
2006-04-06 urbanc 2006-04-06 modified the perm_compose rule such that it is applied as simplification rule (as simproc) in the restricted case where the first permutation is a swapping coming from a supports problem also deleted the perm_compose' rule from the set of rules that are automatically tried
2006-04-06 haftmann 2006-04-06 cleanup in typedef/datatype package
2006-04-06 haftmann 2006-04-06 added explicit serialization for int equality
2006-04-06 haftmann 2006-04-06 adapted for definitional code generation
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;