NEWS
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
2001-05-18 nipkow 2001-05-18 *** empty log message ***
2001-04-09 paulson 2001-04-09 Isar hint
2001-02-23 oheimb 2001-02-23 renamed addaltern to addafter, addSaltern to addSafter
2001-02-21 oheimb 2001-02-21 added split_conv_tac (also to claset()) as an optimization
2001-02-20 oheimb 2001-02-20 made split_all_tac safe introducing safe_full_simp_tac, EXISTING PROOFS MAY FAIL
2001-02-15 oheimb 2001-02-15 added missiong word
2001-02-14 wenzelm 2001-02-14 isatool install handles KDE version 1 or 2;
2001-02-13 wenzelm 2001-02-13 tuned;
2001-02-11 wenzelm 2001-02-11 more robust selection of calculational rules;
2001-02-11 wenzelm 2001-02-11 tuned;
2001-02-10 ballarin 2001-02-10 Updates to HOL/Algebra: - axclasses consolidated (lemma one_not_zero) - summation operator SUM removed, now uses setsum Use of setsum made it necessary to relax sort constraint in its definition to {zero, plus}.
2001-02-05 wenzelm 2001-02-05 tuned;
2001-02-04 wenzelm 2001-02-04 * no_document ML operator temporarily disables LaTeX document generation;