src/HOL/Auth/OtwayReesBella.thy
2015-07-18 wenzelm 2015-07-18 prefer tactics with explicit context;
2015-02-10 wenzelm 2015-02-10 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2013-04-27 wenzelm 2013-04-27 uniform Proof.context for hyp_subst_tac;
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2011-11-20 wenzelm 2011-11-20 eliminated obsolete "standard";
2011-09-12 nipkow 2011-09-12 new fastforce replacing fastsimp - less confusing name
2010-09-09 paulson 2010-09-09 Tidied up proofs using sledgehammer, also deleting unnecessary semicolons
2010-07-22 wenzelm 2010-07-22 updated some headers;
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-03-16 wenzelm 2009-03-16 simplified method setup;
2009-03-13 wenzelm 2009-03-13 unified type Proof.method and pervasive METHOD combinators;
2007-08-01 wenzelm 2007-08-01 tuned ML bindings (for multithreading);
2007-07-11 berghofe 2007-07-11 Adapted to new inductive definition package.
2006-11-29 wenzelm 2006-11-29 simplified method setup;
2006-07-08 wenzelm 2006-07-08 tactic/method simpset: maintain proper context;
2006-02-01 paulson 2006-02-01 new and updated protocol proofs by Giamp Bella