NEWS
2005-06-11 wenzelm 2005-06-11 * Pure/sign/theory: discontinued named name spaces; * Pure: Theory.axioms_of, PureThy.thms_of etc.;
2005-06-05 wenzelm 2005-06-05 * ML: replaced File.sysify_path/quote_sysify_path by File.platform_path/shell_path; tuned;
2005-06-04 wenzelm 2005-06-04 major reorganization and cleanup;
2005-06-02 wenzelm 2005-06-02 tuned;
2005-06-01 ballarin 2005-06-01 Locales: new element constrains, parameter renaming with syntax, experimental command instantiate withdrawn.
2005-05-31 wenzelm 2005-05-31 ML Pure: name spaces have been refined; ML Pure: cases produced by proof methods specify options, NONE means to removee bindings;
2005-05-30 kleing 2005-05-30 typo
2005-05-30 kleing 2005-05-30 updated para on searching
2005-05-27 ballarin 2005-05-27 Typo.
2005-05-27 ballarin 2005-05-27 Locale expressions: rename with optional mixfix syntax.
2005-05-23 wenzelm 2005-05-23 * Pure/Syntax: In schematic variable names, *any* symbol following \<^isub> or \<^isup> is now treated as part of the base name;
2005-05-23 nipkow 2005-05-23 tuned trace info (depth)
2005-05-22 wenzelm 2005-05-22 removed find_rewrites (superceded by improved thms_containing);
2005-05-18 kleing 2005-05-18 searching for combination of criteria (intro, elim, dest, name, pattern)
2005-05-17 wenzelm 2005-05-17 tuned;
2005-05-17 wenzelm 2005-05-17 tuned;
2005-05-06 haftmann 2005-05-06 added new antiquotations
2005-04-29 kleing 2005-04-29 new thms_containing that searches for patterns instead of constants (by Rafal Kolanski, NICTA)
2005-04-26 wenzelm 2005-04-26 allow symlinks to all proper Isabelle executables; isabelle-process: Poly/ML no longer needs Perl to run an interactive session;
2005-04-21 wenzelm 2005-04-21 superceded by Pure.thy and CPure.thy;
2005-04-20 gagern 2005-04-20 Allow symlinks to shell scripts
2005-04-19 webertj 2005-04-19 refute extended
2005-04-18 ballarin 2005-04-18 Interpretation supports statically scoped attributes; documentation.
2005-04-16 wenzelm 2005-04-16 Pure: command 'no_syntax' removes grammar declarations;
2005-04-13 wenzelm 2005-04-13 Locales: proper static binding of attribute syntax; Attributes 'induct' and 'cases': support local type or set names;
2005-04-13 wenzelm 2005-04-13 *** MESSAGE REFERS TO PREVIOUS VERSION *** ISABELLE_DOC_FORMAT setting specifies preferred document format; some cleanup;
2005-04-13 wenzelm 2005-04-13 *** empty log message ***
2005-04-11 ballarin 2005-04-11 First release of interpretation commands.
2005-04-07 nipkow 2005-04-07 *** empty log message ***
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-16 nipkow 2005-02-16 *** empty log message ***
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2005-02-11 ballarin 2005-02-11 New reference Toplevel.debug for verbose printing of exns.
2005-02-01 paulson 2005-02-01 the new subst tactic, by Lucas Dixon
2005-01-28 kleing 2005-01-28 -H false for showing proofs (not -H true)
2005-01-27 berghofe 2005-01-27 - Proofs are now hidden by default when generating documents - New syntax for referring to theorems in lists - Improvements to theory loader (relative and absolute paths)
2005-01-24 paulson 2005-01-24 thin_tac now works on P==>Q
2005-01-11 berghofe 2005-01-11 Option for hiding proof scripts in documents.
2004-12-18 schirmer 2004-12-18 added simproc for Let
2004-12-13 nipkow 2004-12-13 *** empty log message ***
2004-12-02 nipkow 2004-12-02 *** empty log message ***
2004-12-01 nipkow 2004-12-01 *** empty log message ***
2004-12-01 kleing 2004-12-01 new antiquotations @{lhs thm} and @{rhs thm}
2004-11-24 nipkow 2004-11-24 *** empty log message ***
2004-11-15 webertj 2004-11-15 minor rewording
2004-11-12 webertj 2004-11-12 isatool usedir -f
2004-10-12 nipkow 2004-10-12 *** empty log message ***
2004-09-27 ballarin 2004-09-27 Modified locales: improved implementation of "includes".
2004-09-13 nipkow 2004-09-13 *** empty log message ***
2004-08-29 webertj 2004-08-29 Provers/blast.ML: depth_limit
2004-08-23 webertj 2004-08-23 new isatool dimacs2hol
2004-08-19 nipkow 2004-08-19 *** empty log message ***
2004-08-16 nipkow 2004-08-16 *** empty log message ***
2004-08-12 ballarin 2004-08-12 Disallowed "includes" in locale declarations.
2004-08-06 nipkow 2004-08-06 undid UN/INT xsymbol syntax with subscripts.
2004-08-03 ballarin 2004-08-03 New transitivity reasoners for transitivity only and quasi orders.
2004-07-30 wenzelm 2004-07-30 ZF/Simplifier: second copy of context type solver;
2004-07-26 ballarin 2004-07-26 New prover for transitive and reflexive-transitive closure of relations. - Code in Provers/trancl.ML - HOL: Simplifier set up to use it as solver
2004-07-22 nipkow 2004-07-22 *** empty log message ***
2004-07-15 nipkow 2004-07-15 *** empty log message ***