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;

support for ``indexed syntax'' (using "\<index>" argument instead of "_");

removed special treatment of "_" in syntax (now covered by \<index> arg);

tuned locale interface;

proper treatment of internal parameters;

\usepackage[latin1]{inputenc};

Wenzel:2001:Isar-examples;

updated;

mixfix syntax for selectors;

record: mixfix;

export used_types; tuned;

Locale.activate_context;

beginning support for type instantiation; tuned internal arrangements;

varify returns newly introduced variables;

varifyT' returns newly introduces variables;

added invent_type_names; added add_tvarsT etc. (from drule.ML);

changed Thm.varifyT';

type_env;

added type_env function; let norm_type_XXX work directly with type env component;

export add_tvarsT etc.;

changed Type.varify;

Term.invent_type_names;

*** empty log message ***

*** empty log message ***

made SML/XL happy;

*** empty log message ***

Terminator now uses arith_tac as well.

comp -> rel_comp

isatool expandshort;

Relaxed the precondition of UN_upper_le

isatool expandshort;

new rewrite rules for use by arith_tac to take care of uminus. mods due to reorienting and renaming of real_minus_mult_eq1/2

new rewrite rules for use by arith_tac to take care of uminus.

mods due to reorienting and renaming of real_minus_mult_eq1/2

tuned conversion from terms to "polynomials" for arith_tac: takes care of "uminus" now.

drop_judgment: be graceful about undeclared judgment;

obsolete;

option "-d pdf" by default (accomodates pdf bias of Mac OS X); tuned getpwnam;

removed installfonts, xterm interface; improved default of PROOFGENERAL_OPTIONS;

Removed pointless backtracking from arith_tac

Improved error messages.

*** empty log message ***

tuned;

obsolete;

obsolete;

tuned;

\isasymindex made text mode;

isatools "symbolinput" and "nonascii" have disappeared;

added HOL-Library;

tuned;

updated;

removed altogether;

removed unused stuff;

Updated.

oops;

bounded abstraction now uses syntax "%" / "\<lambda>" instead of "lam";

updated reserved words of HOL;