NEWS
2010-08-19 wenzelm 2010-08-19 merged
2010-08-19 haftmann 2010-08-19 deglobalized named HOL constants
2010-08-18 haftmann 2010-08-18 merged
2010-08-18 haftmann 2010-08-18 NEWS
2010-08-18 haftmann 2010-08-18 more helpful NEWS entry
2010-08-17 haftmann 2010-08-17 preemptive NEWS
2010-08-18 haftmann 2010-08-18 NEWS
2010-08-18 haftmann 2010-08-18 deglobalization
2010-08-17 wenzelm 2010-08-17 discontinued support for Poly/ML 5.0 and 5.1 versions;
2010-08-17 haftmann 2010-08-17 NEWS and CONTRIBUTORS
2010-08-11 haftmann 2010-08-11 NEWS
2010-08-03 wenzelm 2010-08-03 theory loading: only the master source file is looked-up in the implicit load path;
2010-07-31 ballarin 2010-07-31 Documentation of 'interpret' updated.
2010-07-22 wenzelm 2010-07-22 discontinued special treatment of ML files -- no longer complete extensions on demand; simplified Thy_Load.check_file, with uniform error reporting; added Thy_Load.test_file for non-strict checking; misc tuning and simplification;
2010-07-21 wenzelm 2010-07-21 ML antiquotations @{theory} and @{theory_ref} refer to the theory ancestry, not any accidental theory loader state; recovered @{theory_ref NAME} (cf. 1f09a22a1027);
2010-07-14 haftmann 2010-07-14 export_code without file prints to standard output
2010-07-07 bulwahn 2010-07-07 added NEWS entry
2010-07-02 haftmann 2010-07-02 fixed spelling
2010-07-01 haftmann 2010-07-01 "prod" and "sum" replace "*" and "+" respectively; qualified constants Set.member and Set.Collect
2010-07-01 hoelzl 2010-07-01 Updated NEWS
2010-06-29 haftmann 2010-06-29 merged
2010-06-28 haftmann 2010-06-28 dropped ancient infix mem; refined code generation operations in List.thy
2010-06-28 haftmann 2010-06-28 merged constants "split" and "prod_case"
2010-06-25 wenzelm 2010-06-25 explicit treatment of UTF8 sequences as Isabelle symbols;
2010-06-21 wenzelm 2010-06-21 merged, resolving conflicts in doc-src/IsarRef/Thy/HOL_Specific.thy;
2010-06-15 haftmann 2010-06-15 added code_simp infrastructure
2010-06-15 haftmann 2010-06-15 merged
2010-06-14 haftmann 2010-06-14 NEWS
2010-06-14 haftmann 2010-06-14 removed simplifier congruence rule of "prod_case"
2010-06-10 haftmann 2010-06-10 qualified type "*"; qualified constants Pair, fst, snd, split
2010-06-08 haftmann 2010-06-08 qualified types "+" and nat; qualified constants Ball, Bex, Suc, curry; modernized some specifications
2010-06-07 wenzelm 2010-06-07 back to non-release mode;
2010-06-21 wenzelm 2010-06-21 final tuning;
2010-06-11 wenzelm 2010-06-11 NEWS: IsabelleText font;
2010-06-07 berghofe 2010-06-07 Documented changes in induct, cases, and nominal_induct method.
2010-06-07 wenzelm 2010-06-07 more NEWS;
2010-06-07 wenzelm 2010-06-07 more NEWS; tuned;
2010-06-04 krauss 2010-06-04 NEWS (more strict internal axioms/defs format)
2010-06-04 wenzelm 2010-06-04 spelling;
2010-06-03 wenzelm 2010-06-03 diagnostic commands 'ML_val' and 'ML_command' may refer to antiquotations @{Isar.state} and @{Isar.goal};
2010-06-03 krauss 2010-06-03 clarified
2010-06-03 krauss 2010-06-03 mention unconstrain in NEWS
2010-06-02 wenzelm 2010-06-02 improved parallelism of proof term normalization;
2010-06-01 blanchet 2010-06-01 merged
2010-06-01 blanchet 2010-06-01 update NEWS
2010-06-01 blanchet 2010-06-01 removed "nitpick_intro" attribute -- Nitpick noew uses Spec_Rules instead
2010-06-01 blanchet 2010-06-01 added "atoms" option to Nitpick (request from Karlsruhe) + wrap Refute. functions to "nitpick_util.ML"
2010-05-31 wenzelm 2010-05-31 notes on Isabelle/jEdit;
2010-05-31 wenzelm 2010-05-31 modernized some structure names, keeping a few legacy aliases;
2010-05-27 wenzelm 2010-05-27 merged
2010-05-27 boehmes 2010-05-27 merged
2010-05-27 boehmes 2010-05-27 moved SMT into the HOL image
2010-05-27 wenzelm 2010-05-27 renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
2010-05-27 wenzelm 2010-05-27 renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
2010-05-27 wenzelm 2010-05-27 misc updates for release;
2010-05-27 wenzelm 2010-05-27 constant Rat.normalize needs to be qualified;
2010-05-22 huffman 2010-05-22 NEWS: removed fixrec_simp attribute
2010-05-20 haftmann 2010-05-20 turned old-style mem into an input abbreviation
2010-05-18 huffman 2010-05-18 remove several redundant lemmas about floor and ceiling
2010-05-18 wenzelm 2010-05-18 merged