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
1996-06-25 berghofe 1996-06-25 Changed argument order of nat_rec.
1996-06-25 berghofe 1996-06-25 Changed argument order of nat_rec.
1996-06-21 berghofe 1996-06-21 Replaced occurrence of fast_tac by Fast_tac .
1996-06-21 berghofe 1996-06-21 Replaced occurrence of set_cs by claset_of "Fun" .
1996-06-21 berghofe 1996-06-21 Added function Addss.
1996-06-21 berghofe 1996-06-21 Classical tactics now use default claset.
1996-06-21 oheimb 1996-06-21 minor fix of index_vnames: name "O" is occupied (used in HOL/Relation.thy)
1996-06-20 paulson 1996-06-20 Restored Addsimps [Suc_le_lessD], as it cannot be added to base HOL
1996-06-20 paulson 1996-06-20 Corrected comment
1996-06-18 paulson 1996-06-18 New rewrites for vacuous quantification
1996-06-18 paulson 1996-06-18 Addition of setOfList
1996-06-18 paulson 1996-06-18 Addition of Safe_step_tac
1996-06-18 paulson 1996-06-18 Translation infixes <->, etc., no longer available at top-level
1996-06-18 paulson 1996-06-18 Addition of setOfList
1996-06-18 paulson 1996-06-18 Removal of list_all
1996-06-18 paulson 1996-06-18 Translation infixes <->, etc., no longer available at top-level
1996-06-17 paulson 1996-06-17 Inserted comment about problem 43
1996-06-17 paulson 1996-06-17 Removed quantification over lists
1996-06-17 paulson 1996-06-17 Now exports Delrules
1996-06-17 paulson 1996-06-17 Converted to use constdefs instead of defs
1996-06-14 paulson 1996-06-14 Explicitly included add_mult_distrib & add_mult_distrib2
1996-06-14 paulson 1996-06-14 New example of greatest common divisor
1996-06-14 paulson 1996-06-14 Added Primes to list of theories in target ex
1996-06-14 paulson 1996-06-14 Now del_simp catches the right exception!
1996-06-14 paulson 1996-06-14 Added delete function for brls
1996-06-14 paulson 1996-06-14 Now implements delrules