1996-07-26 paulson 1996-07-26 Auth proofs work up to the XXX...
1996-07-26 paulson 1996-07-26 Proved insert_image
1996-07-26 paulson 1996-07-26 Redefining "range" as a macro
1996-07-26 paulson 1996-07-26 Proved bex_False
1996-07-23 oheimb 1996-07-23 unnecessary files removed
1996-07-23 paulson 1996-07-23 Corrected typo regarding the type of set_oracle
1996-07-22 paulson 1996-07-22 Added insert_commute
1996-07-22 paulson 1996-07-22 Updated BibTeX identifiers
1996-07-22 paulson 1996-07-22 Acknowledged Martin Simons
1996-07-22 paulson 1996-07-22 Corrected typo involving derivations
1996-07-19 berghofe 1996-07-19 Classical tactics now use default claset.
1996-07-17 pusch 1996-07-17 Corrected o_assoc lemma
1996-07-17 pusch 1996-07-17 removed superfluous Park-induct rule
1996-07-17 oheimb 1996-07-17 renamed adm_impl to adm_imp
1996-07-17 paulson 1996-07-17 Edited in response to referees comments; new references
1996-07-17 oheimb 1996-07-17 correction of recent typo
1996-07-16 berghofe 1996-07-16 Added section about current claset.
1996-07-16 paulson 1996-07-16 Put in minimal simpset to avoid excessive simplification, just as in revision 1.9 of HOL/indrule.ML Isabelle94-6
1996-07-16 paulson 1996-07-16 corrected comment
1996-07-16 paulson 1996-07-16 Acknowledged Stefan Berghofer for finding errors
1996-07-16 paulson 1996-07-16 Fixed typo regarding lifting over P|P
1996-07-16 paulson 1996-07-16 Increased revision number
1996-07-16 paulson 1996-07-16 Tidied up; added "syntax" decl
1996-07-15 paulson 1996-07-15 New dummy .thy files to document dependencies
1996-07-15 paulson 1996-07-15 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
1996-07-15 nipkow 1996-07-15 Documented simplification tactics which make use of the implicit simpset.
1996-07-15 berghofe 1996-07-15 updated syntax of primrec definitions
1996-07-12 oheimb 1996-07-12 *** empty log message ***
1996-07-12 oheimb 1996-07-12 bug fix: Glam_ast_tr
1996-07-12 oheimb 1996-07-12 added configuration for STEM
1996-07-12 oheimb 1996-07-12 minor bug fix
1996-07-12 berghofe 1996-07-12 updated syntax of primrec definitions
1996-07-12 oheimb 1996-07-12 replaced setsolver ... by addsolver
1996-07-11 paulson 1996-07-11 Added Msg 3; works up to Says_Server_imp_Key_newK
1996-07-11 paulson 1996-07-11 Corrected indentation
1996-07-11 paulson 1996-07-11 Oracles can now be strings instead of identifiers
1996-07-11 paulson 1996-07-11 Added insert_mono
1996-07-11 paulson 1996-07-11 Added ML reference
1996-07-11 paulson 1996-07-11 Modified to reject certain inputs -- illustrates error handling
1996-07-11 paulson 1996-07-11 Documentation of oracles and their syntax
1996-07-05 berghofe 1996-07-05 Simplified syntax of primrec definitions.
1996-06-28 paulson 1996-06-28 Removed a use of eq_cs
1996-06-28 paulson 1996-06-28 Removed the unused eq_cs, and added some distributive laws
1996-06-28 paulson 1996-06-28 Removed the unused rel_eq_cs
1996-06-28 paulson 1996-06-28 Added contra_subsetD and rev_contra_subsetD
1996-06-28 paulson 1996-06-28 Added rev_notE by analogy with rev_mp
1996-06-28 paulson 1996-06-28 Proving safety properties of authentication protocols
1996-06-28 paulson 1996-06-28 Updated reference to Slinds paper on TFL
1996-06-28 paulson 1996-06-28 Now set_cs is just taken from !claset
1996-06-28 paulson 1996-06-28 Added type-checking to rule "combination". This corrects a fault concerning soundness. See Jeremy Dawsons message of 27 Jun 1996 on isabelle-users
1996-06-28 paulson 1996-06-28 Restored warning comment
1996-06-27 oheimb 1996-06-27 re-added when_funs to library.ML
1996-06-27 oheimb 1996-06-27 patches for Holcfb.thy removed
1996-06-27 oheimb 1996-06-27 removed old version of LEAST operator
1996-06-26 oheimb 1996-06-26 repaired 8bit pragma
1996-06-26 oheimb 1996-06-26 adapted path to 8bit package
1996-06-26 oheimb 1996-06-26 function names in when_rews now meta-quantified
1996-06-26 oheimb 1996-06-26 when_funs removed
1996-06-25 oheimb 1996-06-25 *** empty log message ***
1996-06-25 oheimb 1996-06-25 Initial revision