NEWS
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");
2001-10-21 wenzelm 2001-10-21 * proper spacing of consecutive markup elements, especially text blocks after section headings;
2001-10-20 wenzelm 2001-10-20 * greatly simplified document preparation setup, including more graceful interpretation of isatool usedir -i/-d/-D options, and more instructive isatool mkdir; users should basically be able to get started with "isatool mkdir Test && isatool make"; * theory dependency graph may now be incorporated into documents; isatool usedir -g true will produce session_graph.eps/.pdf for use with \includegraphics of LaTeX;
2001-10-17 wenzelm 2001-10-17 tuned;
2001-10-16 wenzelm 2001-10-16 tuned;
2001-10-16 wenzelm 2001-10-16 * HOL: concrete setsum syntax "\<Sum>i:A. b" == "setsum (%i. b) A" (beware of argument permutation!);
2001-10-16 wenzelm 2001-10-16 tuned;
2001-10-16 wenzelm 2001-10-16 improved induct;
2001-10-15 kleing 2001-10-15 canonical 'cases'/'induct' rules for n-tuples (n=3..7)
2001-10-13 wenzelm 2001-10-13 * HOL: 'typedef' now allows alternative names for Rep/Abs morphisms;
2001-10-13 wenzelm 2001-10-13 * Pure: added 'corollary' command;
2001-10-11 wenzelm 2001-10-11 * Isar/Pure: fixed 'token_translation' command;
2001-10-08 wenzelm 2001-10-08 * added default LaTeX bindings for \<tturnstile> and \<TTurnstile>; note that these symbols are unavailable in Proof General / X-Symbol;
2001-10-05 wenzelm 2001-10-05 *** empty log message ***
2001-10-05 wenzelm 2001-10-05 *** empty log message ***
2001-10-04 wenzelm 2001-10-04 improved proof by cases and induction;
2001-10-04 wenzelm 2001-10-04 * moved induct/cases attributes to Pure, added 'print_induct_rules' command;
2001-10-03 wenzelm 2001-10-03 *** empty log message ***
2001-09-28 wenzelm 2001-09-28 *** empty log message ***
2001-09-27 wenzelm 2001-09-27 HOL: eliminated global items;
2001-09-26 wenzelm 2001-09-26 tuned;
2001-09-08 wenzelm 2001-09-08 * system: support Poly/ML 4.1.1 (large heaps); * system: smart selection of Isabelle process versus Isabelle interface, accomodates case-insensitive file systems (e.g. HFS+);
2001-09-04 wenzelm 2001-09-04 renamed "antecedent" case to "rule_context";
2001-08-31 wenzelm 2001-08-31 * Proof General keywords specification is now part of the Isabelle distribution (see etc/isar-keywords.el);
2001-08-09 oheimb 2001-08-09 renamed addaltern to addafter, addSaltern to addSafter
2001-08-08 wenzelm 2001-08-08 * HOL: syntax translations now work properly with numerals and records expressions;
2001-08-07 wenzelm 2001-08-07 tuned;
2001-08-07 wenzelm 2001-08-07 tuned;
2001-07-20 wenzelm 2001-07-20 HOL: added "The";
2001-07-03 paulson 2001-07-03 GroupTheory
2001-06-05 nipkow 2001-06-05 *** empty log message ***
2001-05-21 paulson 2001-05-21 ZF: division