2002-03-07 wenzelm 2002-03-07 tuned;
2002-03-05 wenzelm 2002-03-05 tuned;
2002-03-05 berghofe 2002-03-05 Added two paragraphs on "rules" method and code generator.
2002-02-28 wenzelm 2002-02-28 fixed date;
2002-02-27 wenzelm 2002-02-27 tuned;
2002-02-21 wenzelm 2002-02-21 * HOL: removed obsolete theorem "optionE";
2002-02-21 wenzelm 2002-02-21 * HOL: removed obsolete theorem "optionE";
2002-02-19 wenzelm 2002-02-19 "isatool usedir -D output HOL Test && isatool document Test/output";
2002-02-14 nipkow 2002-02-14 *** empty log message ***
2002-02-12 wenzelm 2002-02-12 * Isar/Pure: marginal comments ``--'' may now occur just anywhere in the text;
2002-01-26 wenzelm 2002-01-26 Isar cases/induct: no backtracking;
2002-01-25 paulson 2002-01-25 ZF
2002-01-23 wenzelm 2002-01-23 * HOL: nat_number_of;
2002-01-21 wenzelm 2002-01-21 * Pure/show_hyps reset by default (in accordance to existing Isar practice);
2002-01-16 paulson 2002-01-16 Isar version of ZF/AC
2002-01-15 wenzelm 2002-01-15 tuned;
2002-01-15 wenzelm 2002-01-15 Isar: undeclared rule case names default to numbers 1, 2, 3, ...;
2002-01-14 wenzelm 2002-01-14 * system: reduced base memory usage by Poly/ML (approx. 20 MB instead of 40 MB), cf. ML_OPTIONS;
2002-01-13 wenzelm 2002-01-13 * HOL: symbolic syntax for x^2 (numeral 2);
2002-01-13 wenzelm 2002-01-13 HOL-Real/Complex_Numbers;
2002-01-12 wenzelm 2002-01-12 tuned;
2002-01-11 wenzelm 2002-01-11 Isabelle2002 (January 2002);
2002-01-11 wenzelm 2002-01-11 * Pure: localized 'lemmas', 'theorems', 'declare';
2002-01-09 wenzelm 2002-01-09 * added \<euro> symbol; * HOL-Hyperreal is now a logic image; * isatool latex no longer depends on changed TEXINPUTS;
2002-01-03 wenzelm 2002-01-03 tuned;
2001-12-29 wenzelm 2001-12-29 * ZF/IMP: updated and converted to new-style theory format;
2001-12-27 wenzelm 2001-12-27 HOL/IMP and HOLCF/IMP updated and converted (Gerwin Klein);
2001-12-21 wenzelm 2001-12-21 HOL/record: shared operations ("more", "fields", etc.) now need to be always qualified;
2001-12-20 nipkow 2001-12-20 *** empty log message ***
2001-12-20 paulson 2001-12-20 ZF/Main
2001-12-18 wenzelm 2001-12-18 * system: tested support for MacOS X;
2001-12-13 nipkow 2001-12-13 *** empty log message ***
2001-12-11 wenzelm 2001-12-11 tuned;
2001-12-11 wenzelm 2001-12-11 isatools "symbolinput" and "nonascii" have disappeared;
2001-12-10 wenzelm 2001-12-10 * HOL: bounded abstraction now uses syntax "%" / "\<lambda>" instead of "lam" -- INCOMPATIBILITY;
2001-12-06 wenzelm 2001-12-06 * Pure/obtain: "thesis" now internal (use ?thesis); * Pure: generic 'sym' / 'symmetric' attributes; * Provers/classical: 'swapped' attribute; * HOL: proper rules less_induct and wf_induct_rule;
2001-12-05 wenzelm 2001-12-05 * Pure/Provers/classical: simplified integration with pure rule attributes and methods;
2001-12-01 wenzelm 2001-12-01 * HOL: the class of all HOL types is now called "type" rather than "term"; INCOMPATIBILITY, need to adapt references to this type class in axclass/classes, instance/arities, and (usually rare) occurrences in typings (of consts etc.); internally the class is called "HOL.type", ML programs should refer to HOLogic.typeS;
2001-11-28 wenzelm 2001-11-28 * Isar/Pure: "sorry" no longer requires quick_and_dirty in interactive mode; * Pure/syntax: "x::_::foo" sort constraints;
2001-11-24 wenzelm 2001-11-24 tuned;
2001-11-20 wenzelm 2001-11-20 * HOL/record: cases/induct for more parts; * syntax: prefer later print_translation functions;
2001-11-20 paulson 2001-11-20 Hyperreal
2001-11-15 wenzelm 2001-11-15 * ZF: new-style theory commands '(co)inductive', '(co)datatype', 'rep_datatype', 'inductive_cases'; also methods 'ind_cases', 'induct_tac', 'case_tac', and 'typecheck' (with attribute 'TC');
2001-11-13 wenzelm 2001-11-13 * ZF: new-style theory commands 'inductive', 'inductive_cases', and methods 'ind_cases', 'induct_tac', 'case_tac';
2001-11-12 wenzelm 2001-11-12 Isar: 'induct' proper support for mutual induction involving non-atomic rule statements; Isar/Pure: support multiple simultaneous goal statements;
2001-11-12 paulson 2001-11-12 ZF/Induct,UNITY
2001-11-08 wenzelm 2001-11-08 * Isar/Pure: emulation of instantiation tactics (rule_tac, cut_tac, etc.) now consider the syntactic context of assumptions, giving a better chance to get type-inference of the arguments right (this is especially important for locales); * system: refrain from any attempt at filtering input streams; no longer support ``8bit'' encoding of old isabelle font, instead proper iso-latin characters may now be used;
2001-11-06 wenzelm 2001-11-06 * Isar/Pure: proper integration with ``locales''; unlike the original version by Florian Kammueller, Isar locales package high-level proof contexts rather than raw logical ones (e.g. we admit to include attributes everywhere); * Isar/Pure: theory goals now support ad-hoc contexts, which are discharged in the result, as in ``lemma (assumes A and B) K: A .''; syntax coincides with that of a locale body;
2001-11-03 wenzelm 2001-11-03 * 'domain' package adapted to new-style theories, e.g. see HOLCF/ex/Dnat.thy;
2001-11-03 wenzelm 2001-11-03 HOLCF: proper rep_datatype lift (see theory Lift); use plain induct_tac instead of lift.induct_tac, use UU instead of Undef in cases;
2001-10-31 wenzelm 2001-10-31 - 'induct' may now use elim-style induction rules without chaining facts, using ``missing'' premises from the goal state; this allows rules stemming from inductive sets to be applied in unstructured scripts, while still benefitting from proper handling of non-atomic statements; NB: major inductive premises need to be put first, all the rest of the goal is passed through the induction;
2001-10-30 wenzelm 2001-10-30 - 'induct' method now derives symbolic cases from the *rulified* rule (before it used to rulify cases stemming from the internal atomized version); this means that the context of a non-atomic statement becomes is included in the hypothesis, avoiding the slightly cumbersome show "PROP ?case" form;
2001-10-27 wenzelm 2001-10-27 * Pure/axclass: removed obsolete ML interface goal_subclass/goal_arity;
2001-10-26 wenzelm 2001-10-26 * Pure: method 'atomize' presents local goal premises as object-level statements (atomic meta-level propositions); setup controlled via rewrite rules declarations of 'atomize' attribute; example application: 'induct' method with proper rule statements in improper proof *scripts*;
2001-10-25 wenzelm 2001-10-25 * HOL/record: - removed "more" class (simply use "term") -- INCOMPATIBILITY;
2001-10-25 wenzelm 2001-10-25 * Provers: 'simplified' attribute may refer to explicit rules instead of full simplifier context; 'iff' attribute handles conditional rules; * HOL/record: - provides cases/induct rules for use with corresponding Isar methods; - old "make" and "make_scheme" operation removed -- INCOMPATIBILITY; - new derived operations "make" (for adding fields of current record), "extend" to promote fixed record to record scheme, and "truncate" for the reverse; cf. theorems "derived_defs", which are *not* declared as simp by default; - internal definitions directly based on a light-weight abstract theory of product types over typedef rather than datatype;
2001-10-25 wenzelm 2001-10-25 tuned;
2001-10-25 wenzelm 2001-10-25 * HOL/record: - provides cases/induct rules for use with corresponding Isar methods; - "record" operation truncates to particular fixed record (acts like a type cast); - make_defs no longer part of default simps; - internal definitions directly based on a light-weight abstract theory of product types over typedef rather than datatype;
2001-10-24 wenzelm 2001-10-24 * clasimp: ``iff'' declarations now handle conditional rules as well;
2001-10-23 wenzelm 2001-10-23 * Pure: removed obsolete 'exported' attribute; * Pure: dummy pattern "_" in is/let is now automatically ``lifted'' over bound variables: "ALL x. P x --> Q x" (is "ALL x. _ --> ?C x") supersedes more cumbersome ... (is "ALL x. _ x --> ?C x");