Proved insert_image

Redefining "range" as a macro

Proved bex_False

unnecessary files removed

Corrected typo regarding the type of set_oracle

Added insert_commute

Updated BibTeX identifiers

Acknowledged Martin Simons

Corrected typo involving derivations

Classical tactics now use default claset.

Corrected o_assoc lemma

removed superfluous Park-induct rule

renamed adm_impl to adm_imp

Edited in response to referees comments; new references

correction of recent typo

Added section about current claset.

Put in minimal simpset to avoid excessive simplification, just as in revision 1.9 of HOL/indrule.ML

corrected comment

Acknowledged Stefan Berghofer for finding errors

Fixed typo regarding lifting over P|P

Increased revision number

Tidied up; added "syntax" decl

New dummy .thy files to document dependencies

Uses minimal simpset (min_ss) and full_simp_tac instead of asm_full_simp_tac to prevent excessive simplification, which can cause proofs to fail

Documented simplification tactics which make use of the implicit simpset.

updated syntax of primrec definitions

*** empty log message ***

bug fix: Glam_ast_tr

added configuration for STEM

minor bug fix

updated syntax of primrec definitions

replaced setsolver ... by addsolver

Added Msg 3; works up to Says_Server_imp_Key_newK

Corrected indentation

Oracles can now be strings instead of identifiers

Added insert_mono

Added ML reference

Modified to reject certain inputs -- illustrates error handling

Documentation of oracles and their syntax

Simplified syntax of primrec definitions.

Removed a use of eq_cs

Removed the unused eq_cs, and added some distributive laws

Removed the unused rel_eq_cs

Added contra_subsetD and rev_contra_subsetD

Added rev_notE by analogy with rev_mp

Proving safety properties of authentication protocols

Updated reference to Slinds paper on TFL

Now set_cs is just taken from !claset

Added type-checking to rule "combination". This corrects a fault concerning soundness. See Jeremy Dawsons message of 27 Jun 1996 on isabelle-users

Restored warning comment

re-added when_funs to library.ML

patches for Holcfb.thy removed

removed old version of LEAST operator

repaired 8bit pragma

adapted path to 8bit package

function names in when_rews now meta-quantified

when_funs removed

*** empty log message ***

Initial revision

Changed argument order of nat_rec.

Changed argument order of nat_rec.

Replaced occurrence of fast_tac by Fast_tac .

Replaced occurrence of set_cs by claset_of "Fun" .

Added function Addss.

Classical tactics now use default claset.

minor fix of index_vnames: name "O" is occupied (used in HOL/Relation.thy)

Restored Addsimps [Suc_le_lessD], as it cannot be added to base HOL

Corrected comment

New rewrites for vacuous quantification

Addition of setOfList

Addition of Safe_step_tac

Translation infixes <->, etc., no longer available at top-level

Addition of setOfList

Removal of list_all

Translation infixes <->, etc., no longer available at top-level

Inserted comment about problem 43

Removed quantification over lists

Now exports Delrules

Converted to use constdefs instead of defs

Explicitly included add_mult_distrib & add_mult_distrib2

New example of greatest common divisor

Added Primes to list of theories in target ex

Now del_simp catches the right exception!

Added delete function for brls

Now implements delrules

Added new Primes theory

Explicitly included add_mult_distrib & add_mult_distrib2

Updated list of theories for target ex

Tidied spacing

New lemmas for gcd example

Obsolete relics concerned with recursion

New example of GCDs and divides relation

The "divides" relation, the greatest common divisor and Euclid's algorithm

Addition of converse_iff, domain_converse, range_converse as rewrites

Quotes now optional around inductive set

Quotes now optional around inductive set