NEWS
2000-09-15 wenzelm 2000-09-15 system: isatool installfonts may handle X-Symbol fonts as well;
2000-09-15 paulson 2000-09-15 renamed the select rules
2000-09-12 wenzelm 2000-09-12 renamed atts: rulify to rule_format, elimify to elim_format;
2000-09-12 wenzelm 2000-09-12 replaced "delrule" by "rule del";
2000-09-07 wenzelm 2000-09-07 HOL: qed_spec_mp now also removes bounded ALL; Isar: renamed some attributes;
2000-09-06 nipkow 2000-09-06 *** empty log message ***
2000-09-05 paulson 2000-09-05 meson_tac
2000-09-02 wenzelm 2000-09-02 * HOL/Lambda: converted into new-style theory and document;
2000-08-30 wenzelm 2000-08-30 tuned;
2000-08-30 nipkow 2000-08-30 *** empty log message ***
2000-08-30 wenzelm 2000-08-30 fixed name;
2000-08-30 nipkow 2000-08-30 *** empty log message ***
2000-08-29 wenzelm 2000-08-29 * 'pr' command: optional argument for ProofContext.prems_limit;
2000-08-29 wenzelm 2000-08-29 * Isar/Provers: 'simp' method now supports 'cong' modifiers; * Provers: Simplifier.easy_setup; tuned;
2000-08-28 wenzelm 2000-08-28 * \isabellestyle{it} produces near math mode output; * settings: smart setup of canonical ML_HOME, ISABELLE_INTERFACE, XSYMBOL_HOME;
2000-08-18 paulson 2000-08-18 new example ZF/ex/NatSum
2000-08-17 wenzelm 2000-08-17 Isar/Pure: renamed 'RS' attribute to 'THEN'; Isar/Provers: added 'arith_split' attribute; Isar/Provers: added 'fastsimp' and 'clarsimp' methods; Isar/HOL/inductive: rename "intrs" to "intros"; HOL/record: added general record equality rule to simpset;
2000-08-11 paulson 2000-08-11 ZF arith
2000-08-07 paulson 2000-08-07 ZF arith
2000-08-01 wenzelm 2000-08-01 * blast(_tac) now handles actual object-logic rules as assumptions; note that auto(_tac) uses blast(_tac) internally, too; tuned;
2000-07-28 nipkow 2000-07-28 * HOL/While
2000-07-25 wenzelm 2000-07-25 * Isar/Provers: intro/elim/dest attributes: changed intro/intro!/intro!! flags to intro!/intro/intro? (in most cases, one should have to change intro!! to intro? only);
2000-07-21 oheimb 2000-07-21 strengthened force_tac by using new first_best_tac
2000-07-19 paulson 2000-07-19 // change; also moved entry for AddIffs
2000-07-18 wenzelm 2000-07-18 * HOL: removed obsolete expand_if = split_if; theorems if_splits = split_if split_if_asm; datatype package provides theorems foo.splits = foo.split foo.split_asm for each datatype;
2000-07-16 wenzelm 2000-07-16 * tuned AST representation of nested pairs, avoiding bogus output in case of overlap with user translations (e.g. judgements over tuples); * AST translation rules no longer require constant head on LHS;
2000-07-14 paulson 2000-07-14 AddIffs
2000-07-13 wenzelm 2000-07-13 HOL: the disjoint sum is now "<+>" instead of "Plus"; ML: PureThy.add_defs gets additional argument;
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;