2006-04-09 nipkow 2006-04-09 Made "empty" an abbreviation.
2006-04-09 nipkow 2006-04-09 *** empty log message ***
2006-04-09 nipkow 2006-04-09 Removed old set interval syntax.
2006-04-08 wenzelm 2006-04-08 pretty_term: late externing of consts (support authentic syntax);
2006-04-08 wenzelm 2006-04-08 pretty: late externing of consts (support authentic syntax);
2006-04-08 wenzelm 2006-04-08 removed fix_mixfix; added const_mixfix, mixfix_const;
2006-04-08 wenzelm 2006-04-08 abbreviation(_i): do not expand abbreviations, do not use derived_def;
2006-04-08 wenzelm 2006-04-08 add_abbrevs(_i): support print mode; pretty_term': expand abbreviations only for well-typed terms; added expand_abbrevs; tuned;
2006-04-08 wenzelm 2006-04-08 abbrevs: support print mode;
2006-04-08 wenzelm 2006-04-08 simplified handling of authentic syntax (cf. early externing in consts.ML); simplified extern_term;
2006-04-08 wenzelm 2006-04-08 'abbreviation': optional print mode;
2006-04-08 wenzelm 2006-04-08 tuned;
2006-04-08 wenzelm 2006-04-08 pretty_term': early vs. late externing (support authentic syntax); add_abbrevs(_i): support print mode and authentic syntax;
2006-04-08 wenzelm 2006-04-08 print_theory: print abbreviations nicely;
2006-04-08 wenzelm 2006-04-08 added intern/extern/extern_early; added expand_abbrevs flag; strip_abss: demand ocurrences of bounds in body; const decl: added flag for early externing (disabled for authentic syntax); abbrevs: support print mode; major cleanup;
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