src/HOL/Auth/NS_Public.ML
1997-02-15 oheimb 1997-02-15 reflecting my recent changes of the simplifier and classical reasoner
1997-01-23 paulson 1997-01-23 Tidied proofs by using "etac rev_mp" instead of applying rev_mp to result()
1997-01-17 paulson 1997-01-17 Now with Andy Gordon's treatment of freshness to replace newN/K
1997-01-09 paulson 1997-01-09 New treatment of nonce creation
1997-01-07 paulson 1997-01-07 Tidied up the unicity proofs
1996-12-19 paulson 1996-12-19 Extensive tidying and simplification, largely stemming from changing newN and newK to take an integer argument
1996-12-16 paulson 1996-12-16 New tactics: prove_unique_tac and analz_induct_tac
1996-12-13 paulson 1996-12-13 Streamlined many proofs
1996-12-05 paulson 1996-12-05 Minor speedups
1996-12-05 paulson 1996-12-05 Public-key examples