NEWS
2000-07-12 wenzelm 2000-07-12 infix 'OF' is a version of 'MRS' with more appropriate argument order;
2000-07-04 wenzelm 2000-07-04 * added 'nothing' --- the empty list of theorems;
2000-07-01 wenzelm 2000-07-01 * Isar/HOL/Calculation: new rules for substitution in inequalities (monotonicity conditions are extracted to be proven terminally);
2000-07-01 wenzelm 2000-07-01 * Isar: removed 'help' command, which hasn't been too helpful anyway; should instead use individual commands for printing items (print_commands, print_methods etc.);
2000-06-29 wenzelm 2000-06-29 * formal comments (text blocks etc.) in new-style theories may now contain antiquotations of thm/prop/term/typ to be presented according to latex print mode; concrete syntax is like this: @{term[show_types] "f(x) = a + x"}; * Isar: theory command 'method_setup' provides a simple interface for definining proof methods in ML;
2000-06-29 paulson 2000-06-29 weak elimination rules
2000-06-16 paulson 2000-06-16 real simprocs
2000-06-09 wenzelm 2000-06-09 * browser info session directories are now self-contained (may be put on WWW server seperately);
2000-06-07 wenzelm 2000-06-07 provide TAGS file for Isabelle sources;
2000-06-02 oheimb 2000-06-02 added HOL/Prolog
2000-05-31 wenzelm 2000-05-31 Isar/Pure: removed obsolete 'transfer' attribute (transfer of thms to the current context is now done automatically);
2000-05-30 wenzelm 2000-05-30 * ML: renamed flags Syntax.trace_norm_ast to Syntax.trace_ast; global timing flag supersedes proof_timing and Toplevel.trace;
2000-05-28 wenzelm 2000-05-28 case 'antecedent';
2000-05-25 paulson 2000-05-25 overloading of 0
2000-05-23 nipkow 2000-05-23 SetInterval
2000-05-22 wenzelm 2000-05-22 * Pure: changed syntax of local blocks from {{ }} to { }; * Pure: syntax of sorts made inner, i.e. have to write "{a, b, c}";
2000-05-18 wenzelm 2000-05-18 * HOL/ML: even fewer consts are declared as global (see theories Ord, Lfp, Gfp, WF); this only affects ML packages that refer to const names internally; * 'pr' command: no longer prints theory contexts, but only proof states;
2000-05-10 wenzelm 2000-05-10 tuned;
2000-05-08 paulson 2000-05-08 more details
2000-05-04 paulson 2000-05-04 simprocs
2000-04-18 paulson 2000-04-18 new simprocs for numerals of type "nat"
2000-04-17 wenzelm 2000-04-17 * improved name spaces: ambiguous output is qualified; support for hiding of names;
2000-04-13 nipkow 2000-04-13 *** empty log message ***
2000-04-05 wenzelm 2000-04-05 Isar: simplified (more robust) goal selection of proof methods; Isar: tuned 'let' syntax: replace 'as' keyword by 'and';
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;