tuned ``syntax (output)'';

isatool document: stderr to stdout;

tuned;

document preparation overview;

beginnings of concrete syntax;

include typedef image without path prefix!

updated;

link Types/typedef images;

Isar version; support constdefs, too;

tuned msg;

\CONSTDEFS;

tuned;

next round of updates;

Some new theorems for ordinals

tuned;

first stage of major update;

added zf.tex;

added isabelle-intro, isabelle-logics;

added \indexisarcmdof, \indexisarmethof, \indexisarattof; added \COROLLARYNAME, \COROLLARY;

New theorems by Sidi Ehmety

Literal arithmetic: raising numbers to powers (nat, int, real, hypreal)

Added "Executing higher order logic" paper.

Added section on code generator.

tuned document sources;

'inductive_cases': support 'and' form;

* ZF/IMP: updated and converted to new-style theory format;

update by Stephan Merz;

conversion to Isar/ZF

fixed variable-clash bug in make_elim

obsolete;

tuned tracing markup;

tuned tracing_fn markup;

solve rule: tracing instead of priority;

tuned;

IMP/document/root.tex;

warn for spaces in ISABELLE_HOME;

HOL/IMP and HOLCF/IMP updated and converted (Gerwin Klein);

some new theorems

conversion to Isar

tweaked the standard theorems

Resid converted to Isar/ZF

restart: sync_thy_loader instead of overly aggressive touch_all_thys; provisions for persistent sessions;

qualified point.more;

hide base name of "make", "fields", "extend", "truncate", "more", "more_update";

Theory.hide_space_i true;

hide: flag for full/base name;

HOL/record: shared operations ("more", "fields", etc.) now need to be always qualified;

tuned;

updated;

updated;

isatool browser -o;

removed Misc/Translations (text covered by Documents.thy);

Redundant patterns no longer cause errors.

Code generator now adds type constraints to val declarations (to make SML/NJ happy).

tuned;

updated;

removed Types/records.tex;

added add_fixes: derives mssing type scheme from mixfix;

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;

tuned;

added lemma;

generated text;

supplanted by Records.thy;

some text;

\usepackage{marvosym};

document/Records.tex;

turned into proper Isabelle document;

renamed rtrancl_into_rtrancl2 to converse_rtrancl_into_rtrancl

Eliminated "query" syntax.

*** empty log message ***

ZF/Main

Fixed bug in function add.

new hfootref macro for Web links

converted some ZF/Induct examples to Isar

cast_ok and match_exception_entry no longer disabled (thanks to improvement of code generator).

cast_ok no longer disabled (thanks to improvement of code generator).

Implemented higher order modes.

Moved "code" attribute to Pure/codegen.ML

"code" attribute is now managed by basic code generator module.

Declared characteristic equations for < on nat for code generation.

*** empty log message ***

separation of the AC part of Main into Main_ZFC, plus a few new lemmas

hyperlinks in DVI mode

generalize type variables properly: start with occurrences in objects rather than the inner context! tuned interface of generalize;

tuned interface of ProofContext.generalize; tuned;

HOL/IMP: include session graph;

updated;

tuned;

removed preallocated heaps axiom (now in type safety invariant)

updated;

New type definition diagram

added exec_lub

new type definition figure

minor suggestions from Markus

additional material

* system: tested support for MacOS X;

better simplification makes steps redundant

replaced lepoll_lesspoll_lesspoll, lesspoll_lepoll_lesspoll by lesspoll_trans1, lesspoll_trans2

tuned;

use Locale.read/cert_context_statement;

*** empty log message ***

tuned;

improved mixfix_args;

tuned Type.unify; do *not* declare TVar names as used;

simultaneous type-inference of complete context/statement specifications; reorganized code;

tuned interface of unify, param; added paramify_dummies to turn TypeInfer.anyT into unifiable parameter;

tuned Type.unify;

mods due to changed 1-point simprocs (quantifier1).

mods due to improved 1-point simprocs (quantifier1).

mods due to mor powerful simprocs for 1-point rules (quantifier1).

now permutations of quantifiers are allowed as well.

fixed JVMListExample

MicroJava exception merge

temporarily removed JVMListExample

exception merge + cleanup

exception merge, doesn't work yet

exception merge, cleanup, tuned

exceptions

list_all2_rev

removed debug stuff;