2007-09-18 haftmann 2007-09-18 introduced generic concepts for theory interpretators
2007-09-18 haftmann 2007-09-18 separated code for inductive sequences from inductive_codegen.ML
2007-09-18 haftmann 2007-09-18 distinction between regular and default code theorems
2007-09-18 haftmann 2007-09-18 renamed constructor RealC to Ratreal
2007-09-18 haftmann 2007-09-18 renamed constructor RatC to Rational
2007-09-18 haftmann 2007-09-18 clarified evaluation code
2007-09-18 haftmann 2007-09-18 adjusted
2007-09-18 haftmann 2007-09-18 clarified remark
2007-09-18 haftmann 2007-09-18 added script checking for consistency of ML file header
2007-09-18 nipkow 2007-09-18 sorting
2007-09-18 nipkow 2007-09-18 sorting
2007-09-18 nipkow 2007-09-18 Added function package to PreList Added sorted/sort to List Moved qsort from ex to Library
2007-09-17 wenzelm 2007-09-17 change print_mode: CRITICAL;
2007-09-17 wenzelm 2007-09-17 added print_mode_value (CRITICAL);
2007-09-17 wenzelm 2007-09-17 avoid direct access to print_mode;
2007-09-17 wenzelm 2007-09-17 adapted use_text;
2007-09-17 haftmann 2007-09-17 platform-sensitive default location for ATP provers
2007-09-16 wenzelm 2007-09-16 tuned;
2007-09-16 wenzelm 2007-09-16 HOL/Induct/Common_Patterns.thy
2007-09-16 wenzelm 2007-09-16 added Induct/Common_Patterns.thy;
2007-09-16 wenzelm 2007-09-16 moved induct patterns to HOL/Induct/Common_Patterns.thy;
2007-09-16 wenzelm 2007-09-16 use_file: added ``tune'' argument;
2007-09-16 wenzelm 2007-09-16 added structure Posix;
2007-09-16 wenzelm 2007-09-16 with_modes: always CRITICAL;
2007-09-16 wenzelm 2007-09-16 added ML/ml_parse.ML;
2007-09-16 wenzelm 2007-09-16 obsolete;
2007-09-16 wenzelm 2007-09-16 use_text/file: tune text (cf. ML_Parse.fix_ints);
2007-09-16 wenzelm 2007-09-16 use_text/file: tune text (cf. ML_Parse.fix_ints); activate proper int setup;
2007-09-16 wenzelm 2007-09-16 added ml_system_fix_ints; use_text/file: tune text (cf. ML_Parse.fix_ints);
2007-09-16 wenzelm 2007-09-16 added ml_system_fix_ints;
2007-09-16 wenzelm 2007-09-16 removed obsolete Selector token; tuned signature; string syntax: proper escape format;
2007-09-16 wenzelm 2007-09-16 tuned message;
2007-09-16 wenzelm 2007-09-16 Minimal parsing for SML -- fixing integer numerals.
2007-09-16 wenzelm 2007-09-16 added some int constraints (ML_Parse.fix_ints not active here);
2007-09-15 haftmann 2007-09-15 added rudimentary instantiation stub
2007-09-15 haftmann 2007-09-15 added explicit theorems
2007-09-15 haftmann 2007-09-15 delayed evaluation
2007-09-15 haftmann 2007-09-15 clarified class interfaces and internals
2007-09-15 haftmann 2007-09-15 introduced classes
2007-09-15 haftmann 2007-09-15 multi-functional value keyword
2007-09-15 haftmann 2007-09-15 added lemmas for finiteness
2007-09-15 haftmann 2007-09-15 tuned
2007-09-15 haftmann 2007-09-15 fixed title
2007-09-15 wenzelm 2007-09-15 replaced Symbol.is_hex_letter to Symbol.is_ascii_hex;
2007-09-15 wenzelm 2007-09-15 ML_Lex.keywords; tuned comments;
2007-09-15 wenzelm 2007-09-15 tuned comments;
2007-09-15 wenzelm 2007-09-15 replaced Symbol.is_hex_letter to Symbol.is_ascii_hex; tuned Symbol.is_ascii_blank (according to SML syntax);
2007-09-15 wenzelm 2007-09-15 Lexical syntax for SML.
2007-09-15 wenzelm 2007-09-15 added ML/ml_lex.ML;
2007-09-15 wenzelm 2007-09-15 removed redundant OuterLex.make_lexicon;
2007-09-14 krauss 2007-09-14 lexicographic_order method uses "<*mlex*>" instead of "measures" => no longer depends on List.thy
2007-09-14 krauss 2007-09-14 added "<*mlex*>" which lexicographically combines a measure function with a relation
2007-09-14 wenzelm 2007-09-14 moved ML_XXX.ML files to Pure/ML;
2007-09-14 paulson 2007-09-14 tidied
2007-09-14 urbanc 2007-09-14 reverted back to the old version of the equivariance lemma for ALL
2007-09-13 urbanc 2007-09-13 some cleaning up to do with contexts
2007-09-13 berghofe 2007-09-13 Generalized equivariance and nominal_inductive commands to inductive definitions involving arbitrary monotone operators.
2007-09-13 berghofe 2007-09-13 Added equivariance lemmas for induct_forall.
2007-09-13 berghofe 2007-09-13 Added equivariance lemma for induct_implies.
2007-09-11 webertj 2007-09-11 typo fixed, dead link removed