Cleaned up the code.

New specification syntax added (the specification may be split over several properties).

Allowed for splitting the specification over several lemmas.

Improved handling of modes for equality predicate, to avoid ill-typed ML code due to comparisons between elements of function types.

Fixed problem with "code ind" attribute that caused code generator to fail for mutually recursive predicates.

Added function strong_conn for computing the strongly connected components of the graph.

Change from "tracing" to "warning", as requested by David Aspinall

final tweaks for Isar version

finished conversion to Isar format

new example

new case_tac method

partial conversion to Isar format

partial conversion to Isar format

new case_tac

For the Isar version of the ZF logics manual

converting ex/If to Isar script

A document for UNITY

reformatting change and mention of Introduction to Isabelle

corrections by Viktor Kuncak and minor updating

added tutorial

possibility proof!

ZhouGollmann: new example (fair non-repudiation protocol)

added lemma c_hupd_fst

Modifications after changes in MicroJava/J

Changed lemmas .._type_sound

Added lemma exec_no_xcpt

test_term now renames variable for size of test data to avoid clashes with variables already present in the term to be tested.

cleaned up

*** empty log message ***

Removed extraneous rev in function goal_params (the list of parameters is already reversed by rename_wrt_term).

opened new section for next Isabelle release

test_term now handles Match exception raised in generated code.

Replaced \<leadsto> by \<rightharpoonup>

Simplified a proof using presburger

new theory Library/NatPair

declarations moved from PreList.thy

Fixed two bugs: - presburger_tac now calls ObjectLogic.atomize_tac first to avoid failure when premises contain meta-level quantifiers or implications - The preprocessor now also filters out premises containing variables that are not of type int or nat.

Exported function get_mode.

header comment

new theory NatPair of the injection from nat*nat -> nat

Tidying and replacement of some axioms by specifications

tidied

Added some regression testing for simprocs

fixed simprocs

Added handling of meta implication and meta quantification.

Added handling of free variables (provided they are of sort HOL.type).

Tidied some examples

Added the specification command.

Changed bstring argument to xstring.

*** empty log message ***

Added optional theorem names for the constant definitions added during specification.

Added package for definition by specification.

tidying

Fixing a simproc bug

tidying

Some new thm (ex_map_conv?)

use Library.Some/None instead of just Some/None in generated quickcheck code

Added keywords for random testing.

Restored old (tail recursive!) version of repeat.

Exported function goal_params.

Added several functions for producing random numbers.

Added functions for random testing.

Added generator for test case generators.

mk_int now produces specific constants for 0 and 1.

- Installed specific code generator for equality enforcing that arguments do not have function types, which would result in an error message during compilation. - Added test case generators for basic types.

added upd_fst, upd_snd, some thms

added map_image, restrict_map, some thms

added fold_red, o2l, postfix, some thms

added rev_ballE

re-introduced sort constraints on LHS

corrected markup text

Changed many Intersection rules from i:I to I~=0 to avoid introducing a new variable

~= to neq

converting more theories to Isar scripts, and tidying

Conversion of ZF/UNITY/{FP,Union} to Isar script. Introduction of X-symbols to the ML files.

A patch by david aspinall

Added check for HOL_proofs: Theory WeakNorm is skipped if HOL image has been compiled without proof objects.

converted UNITY/Comp/{AllocImpl,Client} to Isar scripts

converted Counter, Counterc and PriorityAux to Isar scripts (all HOL/UNITY/Comp)

Conversion of UNITY/Comp/Priority.thy to a linear Isar script

Type antiquotations do not use the bracket syntax by default any longer.

moved some lemmas here from ZF

Removal of UNITY/UNITYMisc, moving its theorems elsewhere. Conversion of UNITY/State to Isar format.;

Added DOCTYPE and Content-type to HTML documents.

Moved function for renaming bound variables to Pure/drule.ML

Added functions for renaming bound variables.

Added split_paired_All rule for splitting variables bound by object-level universal quantifiers.

- record_split_tac now also works for object-level universal quantifier - bound variables in split rule now have nicer names - added new simproc record_eq_simproc which prevents simplifier from choosing the "wrong" equality rule

integrated optimizations by Sebastian Skalberg, produces less garbage, is faster and clearer

Conversion of theory UNITY to Isar script

Conversion of AllocBase to new-style

*** empty log message ***

*** empty log message ***

Conversion of "Merge" to Isar format

Conversion of UNITY/Distributor to Isar script. General tidy-up.

Converting ZF/UNITY to Isar

Added new theories StrongNorm and WeakNorm to Lambda example.

Bibliography file with paper by Matthes and Joachimski.

Added bibliography.

Added new theories WeakNorm and StrongNorm.

Added lift_map and subst_map.

Nicer syntax for beta reduction.

Moved strong normalization proof to StrongNorm.thy

New proof of weak normalization with program extraction.

*** empty log message ***

conversion of ClientImpl to Isar script

Adding the theory UNITY/AllocImpl.thy, with supporting lemmas

inserted TUM in other places

added TUM

x-symbols (mostly)

remove -p option, separate setting available

Further tweaks of ZF/UNITY

getting ZF/UNITY working again

Introduction of the theories UNITY/Merge, UNITY/ClientImpl

some new ZF/UNITY material from Sidi Ehmety

examples now use Complex_Main

new theorem

Added term_of function for product type.

Added pair_const.

removed redundant line