2002-01-03 wenzelm 2002-01-03 tuned;
2002-01-03 wenzelm 2002-01-03 next round of updates;
2002-01-03 paulson 2002-01-03 Some new theorems for ordinals
2002-01-02 wenzelm 2002-01-02 tuned;
2002-01-02 wenzelm 2002-01-02 first stage of major update;
2002-01-02 wenzelm 2002-01-02 added zf.tex;
2002-01-02 wenzelm 2002-01-02 added isabelle-intro, isabelle-logics;
2002-01-02 wenzelm 2002-01-02 added \indexisarcmdof, \indexisarmethof, \indexisarattof; added \COROLLARYNAME, \COROLLARY;
2002-01-02 paulson 2002-01-02 New theorems by Sidi Ehmety
2002-01-02 paulson 2002-01-02 Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)
2001-12-31 berghofe 2001-12-31 Added "Executing higher order logic" paper.
2001-12-31 berghofe 2001-12-31 Added section on code generator.
2001-12-29 wenzelm 2001-12-29 tuned document sources;
2001-12-29 wenzelm 2001-12-29 'inductive_cases': support 'and' form;
2001-12-29 wenzelm 2001-12-29 * ZF/IMP: updated and converted to new-style theory format;
2001-12-29 wenzelm 2001-12-29 update by Stephan Merz;
2001-12-28 paulson 2001-12-28 conversion to Isar/ZF
2001-12-28 paulson 2001-12-28 fixed variable-clash bug in make_elim
2001-12-27 wenzelm 2001-12-27 obsolete;
2001-12-27 wenzelm 2001-12-27 tuned tracing markup;
2001-12-27 wenzelm 2001-12-27 tuned tracing_fn markup;
2001-12-27 wenzelm 2001-12-27 solve rule: tracing instead of priority;
2001-12-27 wenzelm 2001-12-27 tuned;
2001-12-27 wenzelm 2001-12-27 IMP/document/root.tex;
2001-12-27 wenzelm 2001-12-27 warn for spaces in ISABELLE_HOME;
2001-12-27 wenzelm 2001-12-27 HOL/IMP and HOLCF/IMP updated and converted (Gerwin Klein);
2001-12-25 paulson 2001-12-25 some new theorems
2001-12-25 paulson 2001-12-25 conversion to Isar
2001-12-22 paulson 2001-12-22 tweaked the standard theorems
2001-12-22 paulson 2001-12-22 Resid converted to Isar/ZF
2001-12-21 wenzelm 2001-12-21 restart: sync_thy_loader instead of overly aggressive touch_all_thys; provisions for persistent sessions;
2001-12-21 wenzelm 2001-12-21 qualified point.more;
2001-12-21 wenzelm 2001-12-21 hide base name of "make", "fields", "extend", "truncate", "more", "more_update";
2001-12-21 wenzelm 2001-12-21 Theory.hide_space_i true;
2001-12-21 wenzelm 2001-12-21 hide: flag for full/base name;
2001-12-21 wenzelm 2001-12-21 HOL/record: shared operations ("more", "fields", etc.) now need to be always qualified;
2001-12-21 wenzelm 2001-12-21 tuned;
2001-12-21 wenzelm 2001-12-21 updated;
2001-12-21 wenzelm 2001-12-21 updated;
2001-12-21 wenzelm 2001-12-21 isatool browser -o;
2001-12-21 wenzelm 2001-12-21 removed Misc/Translations (text covered by Documents.thy);
2001-12-21 berghofe 2001-12-21 Redundant patterns no longer cause errors.
2001-12-21 berghofe 2001-12-21 Code generator now adds type constraints to val declarations (to make SML/NJ happy).
2001-12-21 wenzelm 2001-12-21 tuned;
2001-12-21 wenzelm 2001-12-21 updated;
2001-12-21 wenzelm 2001-12-21 removed Types/records.tex;
2001-12-21 wenzelm 2001-12-21 added add_fixes: derives mssing type scheme from mixfix;
2001-12-21 wenzelm 2001-12-21 fixed inst_thm: proper domain of env; flatten_expr: collective import elements over *all* imports; use ProofContext.add_fixes; disallow term bindings in locale body elements;
2001-12-21 wenzelm 2001-12-21 tuned;
2001-12-20 wenzelm 2001-12-20 added lemma;
2001-12-20 wenzelm 2001-12-20 generated text;
2001-12-20 wenzelm 2001-12-20 supplanted by Records.thy;
2001-12-20 wenzelm 2001-12-20 some text;
2001-12-20 wenzelm 2001-12-20 \usepackage{marvosym};
2001-12-20 wenzelm 2001-12-20 document/Records.tex;
2001-12-20 wenzelm 2001-12-20 turned into proper Isabelle document;
2001-12-20 nipkow 2001-12-20 renamed rtrancl_into_rtrancl2 to converse_rtrancl_into_rtrancl
2001-12-20 berghofe 2001-12-20 Eliminated "query" syntax.
2001-12-20 nipkow 2001-12-20 *** empty log message ***
2001-12-20 paulson 2001-12-20 ZF/Main