NEWS
2008-07-15 wenzelm added command 'linear_undo';
2008-07-14 haftmann unified curried gcd, lcm, zgcd, zlcm
2008-07-11 haftmann Fract now total; improved code generator setup
2008-07-10 wenzelm slightly improved @{lemma} (both for latex and ML);
2008-07-04 huffman HOL-NSA
2008-07-02 haftmann code antiquotation roaring ahead
2008-07-01 haftmann HOL += HOL-Complex
2008-07-01 haftmann HOL += HOL-Complex
2008-06-28 wenzelm tuned;
2008-06-28 wenzelm tuned;
2008-06-28 wenzelm additional ML antiquotations;
2008-06-28 wenzelm @{lemma}: 'by' keyword;
2008-06-28 wenzelm ML: improved antiquotations;
2008-06-23 wenzelm induct_tac: mutual rules work as for method "induct";
2008-06-20 haftmann (removed non-present change)
2008-06-19 wenzelm disposed Sign.read_typ etc;
2008-06-18 wenzelm * Disposed old term read functions;
2008-06-16 wenzelm * Rules and tactics that read instantiations now demand a proper context;
2008-06-14 wenzelm removed exotic 'token_translation' command;
2008-06-13 wenzelm * Recovered hiding of consts;
2008-06-11 wenzelm tuned;
2008-06-10 wenzelm tuned spacing;
2008-06-10 wenzelm * Attributes cases, induct, coinduct support del option.
2008-06-10 wenzelm proper news header;
2008-06-10 haftmann rep_datatype command now takes list of constructors as input arguments
2008-06-03 wenzelm some reorganization and fine-tuning;
2008-06-02 wenzelm reorganized isar-ref;
2008-05-28 wenzelm misc tuning for Isabelle2008;
2008-05-21 berghofe Added entry explaining incompatibilities introduced by replacing sets by predicates.
2008-05-18 wenzelm * Eliminated theory ProtoPure and CPure, leaving just one Pure theory.
2008-05-16 wenzelm * Method "cases", "induct", "coinduct": removed obsolete "(open)" option;
2008-05-15 wenzelm tuned;
2008-05-15 wenzelm * Simplified pdfsetup.sty;
2008-05-13 krauss NEWS about measure functions
2008-05-12 wenzelm misc tuning;
2008-05-02 ballarin unfold_locales part of default method.
2008-04-29 haftmann added lemma antiquotation
2008-04-25 krauss Merged theories about wellfoundedness into one: Wellfounded.thy
2008-04-19 wenzelm NamedThmsFun: removed obsolete print command -- facts are accesible via dynamic name;
2008-04-17 wenzelm * Context-dependent token translations.
2008-04-16 berghofe Added entry for unused_thms command.
2008-04-15 wenzelm added hide fact;
2008-04-15 wenzelm tuned;
2008-04-15 wenzelm * Name space merge now observes canonical order;
2008-04-08 wenzelm support for YXML notation -- XML done right;
2008-04-07 paulson * Metis: the maximum number of clauses that can be produced from a theorem is now given by the attribute max_clauses. Theorems that exceed this number are ignored, with a warning printed.
2008-04-02 haftmann explicit class "eq" for operational equality
2008-03-30 nipkow *** empty log message ***
2008-03-29 wenzelm purely functional setup of claset/simpset/clasimpset;
2008-03-29 wenzelm fixed spelling;
2008-03-29 wenzelm * Eliminated destructive theorem database.
2008-03-27 haftmann explicit case names for rule list_induct2
2008-03-27 wenzelm Command 'setup': discontinued implicit version.
2008-03-27 wenzelm HOL (and FOL): renamed variables in rules imp_elim and swap;
2008-03-25 wenzelm Functor NamedThmsFun: data is available to the user as dynamic fact;
2008-03-24 wenzelm removed obsolete use_legacy_bindings;
2008-03-20 haftmann Theory Product_Type; fixed typos
2008-03-19 wenzelm removed redundant Nat.less_not_sym, Nat.less_asym;
2008-03-19 paulson Attributes sledgehammer_full, sledgehammer_modulus, sledgehammer_sorts
2008-03-18 wenzelm theory loader: discontinued *attached* ML scripts;
less more (0) -1000 -300 -100 -60 tip