| changeset 58860 | fee7cfa69c50 |
| parent 58305 | 57752a91eec4 |
| child 58889 | 5b7a9633cfa8 |
--- a/src/HOL/Auth/Guard/Extensions.thy Sat Nov 01 11:40:55 2014 +0100 +++ b/src/HOL/Auth/Guard/Extensions.thy Sat Nov 01 14:20:38 2014 +0100 @@ -508,7 +508,7 @@ apply (induct evs, simp) apply (rename_tac a b) apply (case_tac a, simp_all) -apply (blast dest: parts_trans)+; +apply (blast dest: parts_trans)+ done subsubsection{*monotonicity of used*}