Improved efficiency of code generated for + and -

Improved efficiency of code generated for < predicate on natural numbers.

Mod due to new thm in Map.

Fixed blunder in the setup of the classical reasoner wrt. the constant "curry".

Added the constant "curry".

*** empty log message ***

Added new theorems

Added a number of thms about map restriction.

Tried to make parser a bit more standard-conforming.

Changed no_vars such that it outputs list of illegal schematic variables.

quantifier symbols

conversion of HOL/Auth/KerberosIV to new-style theory

new, separate specifications

Introduced new syntax for maplets x |-> y

Corrections due to John Matthews

Makes interactive proof scripting recognize the show_all_types flag.

Added 'ambiguity_is_error' flag, which, if set, makes the parser fail, rather than just issue a warning, when the input parsed is ambiguous.

Added show_all_types flag, such that all type information in the term is made explicit.

Method rule_tac understands Isar contexts: documentation.

Methods rule_tac etc support static (Isar) contexts.

Removed the extended digits again.

Fixed typos.

Extended the notion of letter and digit, such that now one may use greek, gothic, euler, or calligraphic letters as normal letters.

Added skalberg to recepients, changed admin from kleing to berghofe.

Converted to new style theories.

Prepared for extended identifiers (\<alpha>, etc.)

Improved the error messages (slightly).

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 ***