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;

* HOL: bounded abstraction now uses syntax "%" / "\<lambda>" instead of "lam" -- INCOMPATIBILITY;

obsolete;

removed additional blank line (confuses some versions of make);

obsolete;

- Changed type of invoke_codegen - Added combinators for sequences

- Added code generator interface for types - Changed type of invoke_codegen

Fixed bug in function find_paths.

Added example file for intuitionistic logic (taken from FOL).

Added support for code generation.

Recursive equations to be used for code generation are now registered via RecfunCodegen.add

Code generator for recursive functions.

Tuned header.

Code generator for datatypes.

Moved contents to files datatype_codegen.ML and recfun_codegen.ML

Turned subcls1 into an inductive relation to make it executable.

Example for code generator.

Added examples for code generator.

Added code generator setup.

Tuned code generator setup.

Added new files (code generator and examples).

Moved code generator setup from Recdef to Inductive.

Replaced several occurrences of "blast" by "rules".

document root;

tuned

HOLCF/IMP converted to Isar

HOL/IMP converted to Isar

converted to Isar

latex output setup

tuned for latex output