1996-07-30 berghofe Classical tactics now use default claset.
1996-07-29 paulson Works up to main theorem, then XXX...X
1996-07-29 paulson Added two new distributive laws
1996-07-26 paulson Addition of rev_notE
1996-07-26 paulson Inserted spaces in error messages to improve readability
1996-07-26 paulson Addition of contra_subsetD and rev_contra_subsetD
1996-07-26 paulson Removal of cfast_tac
1996-07-26 paulson Removed clash with "range" constant
1996-07-26 paulson Redefining "range" as a macro -- new proof needed
1996-07-26 paulson Auth proofs work up to the XXX...
1996-07-26 paulson Proved insert_image
1996-07-26 paulson Redefining "range" as a macro
1996-07-26 paulson Proved bex_False
1996-07-23 oheimb unnecessary files removed
1996-07-23 paulson Corrected typo regarding the type of set_oracle
1996-07-22 paulson Added insert_commute
1996-07-22 paulson Updated BibTeX identifiers
1996-07-22 paulson Acknowledged Martin Simons
1996-07-22 paulson Corrected typo involving derivations
1996-07-19 berghofe Classical tactics now use default claset.
1996-07-17 pusch Corrected o_assoc lemma
1996-07-17 pusch removed superfluous Park-induct rule
1996-07-17 oheimb renamed adm_impl to adm_imp
1996-07-17 paulson Edited in response to referees comments; new references
1996-07-17 oheimb correction of recent typo
1996-07-16 berghofe Added section about current claset.
1996-07-16 paulson Put in minimal simpset to avoid excessive simplification, Isabelle94-6
1996-07-16 paulson corrected comment
1996-07-16 paulson Acknowledged Stefan Berghofer for finding errors
1996-07-16 paulson Fixed typo regarding lifting over P|P
1996-07-16 paulson Increased revision number
1996-07-16 paulson Tidied up; added "syntax" decl
1996-07-15 paulson New dummy .thy files to document dependencies
1996-07-15 paulson Uses minimal simpset (min_ss) and full_simp_tac
1996-07-15 nipkow Documented simplification tactics which make use of the implicit simpset.
1996-07-15 berghofe updated syntax of primrec definitions
1996-07-12 oheimb *** empty log message ***
1996-07-12 oheimb bug fix: Glam_ast_tr
1996-07-12 oheimb added configuration for STEM
1996-07-12 oheimb minor bug fix
1996-07-12 berghofe updated syntax of primrec definitions
1996-07-12 oheimb replaced setsolver ... by addsolver
1996-07-11 paulson Added Msg 3; works up to Says_Server_imp_Key_newK
1996-07-11 paulson Corrected indentation
1996-07-11 paulson Oracles can now be strings instead of identifiers
1996-07-11 paulson Added insert_mono
1996-07-11 paulson Added ML reference
1996-07-11 paulson Modified to reject certain inputs -- illustrates error handling
1996-07-11 paulson Documentation of oracles and their syntax
1996-07-05 berghofe Simplified syntax of primrec definitions.
1996-06-28 paulson Removed a use of eq_cs
1996-06-28 paulson Removed the unused eq_cs, and added some distributive laws
1996-06-28 paulson Removed the unused rel_eq_cs
1996-06-28 paulson Added contra_subsetD and rev_contra_subsetD
1996-06-28 paulson Added rev_notE by analogy with rev_mp
1996-06-28 paulson Proving safety properties of authentication protocols
1996-06-28 paulson Updated reference to Slinds paper on TFL
1996-06-28 paulson Now set_cs is just taken from !claset
1996-06-28 paulson Added type-checking to rule "combination". This corrects a fault
1996-06-28 paulson Restored warning comment
(0) -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip