NEWS
2000-04-01 wenzelm 2000-04-01 recdef: admit name and atts;
2000-03-30 nipkow 2000-03-30 recdef
2000-03-30 wenzelm 2000-03-30 * Isar/Pure: local results and corresponding term bindings are now subject to Hindley-Milner polymorphism (similar to ML); this accommodates incremental type-inference nicely; * Isar/Pure: new calculational elements 'moreover' and 'ultimately' support plain accumulation of results, without applying any rules yet;
2000-03-29 nipkow 2000-03-29 *** empty log message ***
2000-03-24 wenzelm 2000-03-24 HOL/ex/Multiquote;
2000-03-24 wenzelm 2000-03-24 usedir -D: update styles;
2000-03-20 wenzelm 2000-03-20 improved support for emulating tactic scripts;
2000-03-18 wenzelm 2000-03-18 tuned;
2000-03-16 wenzelm 2000-03-16 Isar: splitter support; improved diagnostics; tuned;
2000-03-13 wenzelm 2000-03-13 * HOL: exhaust_tac on datatypes superceded by new case_tac; * ML: PureThy.add_thms/add_axioms/add_defs now return theorems; * Isar/Pure: much better support for case-analysis; * ML: new combinators |>> and |>>>
2000-03-13 nipkow 2000-03-13 *** empty log message ***
2000-03-10 nipkow 2000-03-10 cases_tac
2000-03-09 paulson 2000-03-09 Factorization
2000-03-08 wenzelm 2000-03-08 * isatool mkdir provides easy setup of Isabelle session directories, including proper documents; * generated LaTeX sources are now deleted after successful run (isatool document -c); may retain a copy somewhere else via -D option of isatool usedir; * old-style theories now produce (crude) LaTeX sources as well; * compression of ML heaps images may now be controlled via -c option of isabelle and isatool usedir;
2000-02-22 wenzelm 2000-02-22 * Pure now provides its own version of intro/elim/dest attributes; useful for building new logics, but beware of confusion with the Provers/classical ones! * HOL: removed "case_split" thm binding, should use "cases" proof method anyway; * tuned syntax of "induct" method; * new "cases" method for propositions, inductive sets and types; * HOL/records: admit "r" as field name;
2000-02-21 wenzelm 2000-02-21 HOL/record: fixed select-update simplification procedure to handle extended records as well;
2000-02-07 wenzelm 2000-02-07 intro/elim/dest attributes: changed ! / !! flags to ? / ??;
2000-02-02 wenzelm 2000-02-02 nat as names; obtain; tuned;
1999-11-12 wenzelm 1999-11-12 tuned;
1999-11-11 paulson 1999-11-11 HOL changes
1999-11-11 wenzelm 1999-11-11 header;
1999-10-30 wenzelm 1999-10-30 Isabelle99;
1999-10-22 wenzelm 1999-10-22 tuned simplifier trace output; new flag debug_simp
1999-10-20 wenzelm 1999-10-20 the settings environment is now statically scoped; tuned;
1999-10-14 wenzelm 1999-10-14 document preparation based on (PDF)LaTeX;
1999-10-13 berghofe 1999-10-13 Eliminated mutual_induct_tac.
1999-10-08 wenzelm 1999-10-08 theorem database now also indexes constants "Trueprop", "all", "==>", "=="; thus thms_containing, findI etc. may retrieve more rules;
1999-10-08 wenzelm 1999-10-08 tuned;
1999-10-07 berghofe 1999-10-07 Documented changes to HOL/inductive and function thm_deps.
1999-10-04 wenzelm 1999-10-04 added BVC;
1999-09-29 wenzelm 1999-09-29 proper handling of dangling sort hypotheses (at last!);
1999-09-28 nipkow 1999-09-28 incompatibility solver
1999-09-24 wenzelm 1999-09-24 * HOL/Real/HahnBanach: the Hahn-Banach theorem for real vector spaces (in Isabelle/Isar) -- by Gertrud Bauer;
1999-09-24 wenzelm 1999-09-24 tuned;
1999-09-06 oheimb 1999-09-06 *** empty log message ***
1999-09-03 wenzelm 1999-09-03 added bind_thms;
1999-09-03 paulson 1999-09-03 new SVC url
1999-09-01 wenzelm 1999-09-01 structures Vartab / Termtab (instances of TableFun);
1999-08-23 wenzelm 1999-08-23 tuned;
1999-08-23 wenzelm 1999-08-23 record_simproc;
1999-08-23 nipkow 1999-08-23 simplifier flex heads.
1999-08-23 berghofe 1999-08-23 Moved sum_case to theory HOL/Datatype.
1999-08-21 wenzelm 1999-08-21 real numerals;
1999-08-19 wenzelm 1999-08-19 * HOLCF/IOA/Sequents: renamed 'Cons' to 'Consq' to avoid clash with HOL/List;
1999-08-19 paulson 1999-08-19 defer_recdef
1999-08-19 wenzelm 1999-08-19 tuned;
1999-08-18 wenzelm 1999-08-18 sum_case renamed to basic_sum_case;
1999-08-18 wenzelm 1999-08-18 replaced 'ProofGeneral' by 'Proof General';
1999-08-17 wenzelm 1999-08-17 replaced HOL_quantifiers flag by "HOL" print mode; simplified HOL basic syntax (more orthogonal);
1999-08-16 wenzelm 1999-08-16 tuned;
1999-08-16 wenzelm 1999-08-16 tuned;
1999-08-11 nipkow 1999-08-11 Removed * reset HOL_quantifiers by default, i.e. quantifiers are printed as ALL/EX rather than !/?;
1999-08-09 wenzelm 1999-08-09 theory loader actions;
1999-08-03 paulson 1999-08-03 SVC
1999-07-28 wenzelm 1999-07-28 HOL-Real target now builds an actual image;
1999-07-28 paulson 1999-07-28 LK
1999-07-19 berghofe 1999-07-19 Datatype package now handles arbitrarily branching datatypes.
1999-07-08 wenzelm 1999-07-08 theorems involving oracles are now printed with a suffixed [!];
1999-07-08 paulson 1999-07-08 integer division
1999-06-07 wenzelm 1999-06-07 reset HOL_quantifiers by default;