NEWS
2005-07-06 wenzelm * Pure: Output.time_accumulator;
2005-07-06 wenzelm isatool fixheaders;
2005-07-05 wenzelm tuned;
2005-07-05 wenzelm * Pure: structure OrdList (cf. Pure/General/ord_list.ML);
2005-07-01 wenzelm * Isar profiling: new reference Toplevel.profiling (default 0);
2005-06-24 paulson meson method taking an argument list
2005-06-22 wenzelm * Pure: the Isar proof context type is already defined early in Pure
2005-06-20 wenzelm * Pure: get_thm interface expects datatype thmref;
2005-06-17 wenzelm * Pure/TheoryDataFun: change of the argument structure;
2005-06-11 wenzelm * Pure/sign/theory: discontinued named name spaces;
2005-06-05 wenzelm * ML: replaced File.sysify_path/quote_sysify_path by File.platform_path/shell_path;
2005-06-04 wenzelm major reorganization and cleanup;
2005-06-02 wenzelm tuned;
2005-06-01 ballarin Locales: new element constrains, parameter renaming with syntax,
2005-05-31 wenzelm ML Pure: name spaces have been refined;
2005-05-30 kleing typo
2005-05-30 kleing updated para on searching
2005-05-27 ballarin Typo.
2005-05-27 ballarin Locale expressions: rename with optional mixfix syntax.
2005-05-23 wenzelm * Pure/Syntax: In schematic variable names, *any* symbol following
2005-05-23 nipkow tuned trace info (depth)
2005-05-22 wenzelm removed find_rewrites (superceded by improved thms_containing);
2005-05-18 kleing searching for combination of criteria (intro, elim, dest, name, pattern)
2005-05-17 wenzelm tuned;
2005-05-17 wenzelm tuned;
2005-05-06 haftmann added new antiquotations
2005-04-29 kleing new thms_containing that searches for patterns instead of constants
2005-04-26 wenzelm allow symlinks to all proper Isabelle executables;
2005-04-21 wenzelm superceded by Pure.thy and CPure.thy;
2005-04-20 gagern Allow symlinks to shell scripts
2005-04-19 webertj refute extended
2005-04-18 ballarin Interpretation supports statically scoped attributes; documentation.
2005-04-16 wenzelm Pure: command 'no_syntax' removes grammar declarations;
2005-04-13 wenzelm Locales: proper static binding of attribute syntax;
2005-04-13 wenzelm *** MESSAGE REFERS TO PREVIOUS VERSION ***
2005-04-13 wenzelm *** empty log message ***
2005-04-11 ballarin First release of interpretation commands.
2005-04-07 nipkow *** empty log message ***
2005-03-03 skalberg Move towards standard functions.
2005-02-16 nipkow *** empty log message ***
2005-02-13 skalberg Deleted Library.option type.
2005-02-11 ballarin New reference Toplevel.debug for verbose printing of exns.
2005-02-01 paulson the new subst tactic, by Lucas Dixon
2005-01-28 kleing -H false for showing proofs (not -H true)
2005-01-27 berghofe - Proofs are now hidden by default when generating documents
2005-01-24 paulson thin_tac now works on P==>Q
2005-01-11 berghofe Option for hiding proof scripts in documents.
2004-12-18 schirmer added simproc for Let
2004-12-13 nipkow *** empty log message ***
2004-12-02 nipkow *** empty log message ***
2004-12-01 nipkow *** empty log message ***
2004-12-01 kleing new antiquotations @{lhs thm} and @{rhs thm}
2004-11-24 nipkow *** empty log message ***
2004-11-15 webertj minor rewording
2004-11-12 webertj isatool usedir -f
2004-10-12 nipkow *** empty log message ***
2004-09-27 ballarin Modified locales: improved implementation of "includes".
2004-09-13 nipkow *** empty log message ***
2004-08-29 webertj Provers/blast.ML: depth_limit
2004-08-23 webertj new isatool dimacs2hol
less more (0) -300 -100 -60 tip