NEWS
2004-07-06 schirmer 2004-07-06 * Pure/Namespace: flag unique_names added * Pure/Tactic: print_tac outputs goal through trace channel * HOL/Simplifier: extended record_upd_simproc
2004-06-30 schirmer 2004-06-30 Added reference record_definition_quick_and_dirty_sensitive, to skip proofs triggered by a record definition, if quick_and_dirty is enabled.
2004-06-30 skalberg 2004-06-30 Made simplification procedures simpset-aware.
2004-06-20 wenzelm 2004-06-20 tuned;
2004-06-13 wenzelm 2004-06-13 added display_drafts and print_drafts commands;
2004-06-10 wenzelm 2004-06-10 tuned;
2004-06-10 wenzelm 2004-06-10 tuned;
2004-06-09 wenzelm 2004-06-09 * Document preparation: antiquotations provide option 'locale=NAME';
2004-06-08 paulson 2004-06-08 Groups, Rings and supporting lemmas in ZF
2004-06-06 wenzelm 2004-06-06 HOL: symbolic syntax of Eps;
2004-06-01 wenzelm 2004-06-01 removed obsolete sort 'logic';
2004-05-29 wenzelm 2004-05-29 * ML: all output via channels of writeln etc. passed through Output.output;
2004-05-21 wenzelm 2004-05-21 Pure: clear separation of logical types and nonterminals;
2004-05-10 wenzelm 2004-05-10 Pure: nested comments in inner syntax;
2004-05-06 schirmer 2004-05-06 tuned HOL/record package; enabled record_upd_simproc by default.
2004-05-06 wenzelm 2004-05-06 show_structs option;
2004-05-03 schirmer 2004-05-03 reimplementation of HOL records; only one type is created for each record extension, instead of one type for each field. See NEWS.
2004-05-01 wenzelm 2004-05-01 tuned;
2004-05-01 wenzelm 2004-05-01 improvd indexed syntax and implicit structures; tuned renaming of symbolic identifiers
2004-04-29 wenzelm 2004-04-29 HOLCF: discontinued special version of 'constdefs';
2004-04-22 wenzelm 2004-04-22 Pure: considerably improved version of 'constdefs' command; Pure: 'advanced' translation functions (parse_translation etc.);
2004-04-19 kleing 2004-04-19 add HOL4
2004-04-17 kleing 2004-04-17 added HOL-Matrix, added HOL/Matrix/ROOT.ML
2004-04-16 wenzelm 2004-04-16 Pure: 'instance' now handles general arities;
2004-04-16 berghofe 2004-04-16 Added entry for quickcheck command.
2004-04-15 wenzelm 2004-04-15 tuned;
2004-04-14 schirmer 2004-04-14 * raw control symbols are of the form \<^raw:...> now. * again allowing symbols to begin with "\\" instead of "\" for compatibility with ML-strings of old style theory and ML-files and isa-ProofGeneral.
2004-04-13 wenzelm 2004-04-13 * Calculation commands "moreover" and "also" no longer interfere with current facts ("this"), admitting arbitrary combinations with "then" and derived forms.
2004-04-13 ballarin 2004-04-13 Various changes to HOL-Algebra; Locale instantiation.
2004-04-13 kleing 2004-04-13 isabelle.css
2004-04-12 oheimb 2004-04-12 added HOLCF/Streams.thy (with concatenation etc.)
2004-04-02 ballarin 2004-04-02 Experimental command for instantiation of locales in proof contexts: instantiate <label>: <loc>
2004-03-31 skalberg 2004-03-31 Added check that Theory.ML does not occur in the files section of the theory Theory.
2004-03-24 paulson 2004-03-24 clarified
2004-03-11 webertj 2004-03-11 refute
2004-03-03 schirmer 2004-03-03 added record_ex_sel_eq_simproc
2004-03-01 kleing 2004-03-01 union/intersection over intervals
2004-02-19 paulson 2004-02-19 removal of the legacy ML structure List
2004-02-19 ballarin 2004-02-19 New lemmas about inversion of restricted functions. HOL-Algebra: new locale "ring" for non-commutative rings.
2004-02-19 ballarin 2004-02-19 Efficient, graph-based reasoner for linear and partial orders. + Setup as solver in the HOL simplifier.
2004-02-16 paulson 2004-02-16 arith
2004-02-11 nipkow 2004-02-11 *** empty log message ***
2004-02-04 nipkow 2004-02-04 *** empty log message ***
2004-01-26 schirmer 2004-01-26 * Support for raw latex output in control symbols: \<^raw...> * Symbols may only start with one backslash: \<...>. \\<...> is no longer accepted by the scanner. - Adapted some Isar-theories to fit to this policy
2003-12-29 kleing 2003-12-29 \<^bsub> .. \<^esub>
2003-12-10 ballarin 2003-12-10 Isar: where attribute supports instantiation of type vars.
2003-12-06 kleing 2003-12-06 moreover and also do not reset facts any more
2003-11-14 ballarin 2003-11-14 Type inference bug in Isar attributes "where" and "of" fixed.
2003-11-06 schirmer 2003-11-06 Records: - Record types are now by default printed with their type abbreviation instead of the list of all field types. This can be configured via the reference "print_record_type_abbr". - Simproc "record_upd_simproc" for simplification of multiple updates added (not enabled by default). - Tactic "record_split_simp_tac" to split and simplify records added. - Bug-fix and optimisation of "record_simproc". - "record_simproc" and "record_upd_simproc" are now sensitive to quick_and_dirty flag.
2003-11-06 ballarin 2003-11-06 Isar/Locales: <loc>.intro and <loc>.axioms no longer intro? and elim? by default.
2003-10-22 paulson 2003-10-22 recursion
2003-10-16 paulson 2003-10-16 line-breaks; rewording
2003-10-15 kleing 2003-10-15 use \<^isub> and \<^isup> in identifiers instead of just \<^sub> (avoid conflict with locale subscript syntax)
2003-10-15 kleing 2003-10-15 allow \<^sub> in identifiers
2003-10-09 skalberg 2003-10-09 Added info on the new 'finalconsts' command.
2003-09-30 ballarin 2003-09-30 Improvements to Isar/Locales: premises generated by "includes" elements changed. Bugfix "unify_frozen".
2003-09-23 paulson 2003-09-23 new session HOL-SET-Protocol
2003-08-29 ballarin 2003-08-29 Method rule_tac understands Isar contexts: documentation.
2003-08-29 skalberg 2003-08-29 Removed the extended digits again.
2003-08-28 skalberg 2003-08-28 Fixed typos.