Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Auth/Guard/Guard_NS_Public.thy
changeset 76288 b82ac7ef65ec
parent 76287 cdc14f94c754 
--- a/src/HOL/Auth/Guard/Guard_NS_Public.thy	Thu Oct 13 15:38:32 2022 +0100
+++ b/src/HOL/Auth/Guard/Guard_NS_Public.thy	Thu Oct 13 15:49:09 2022 +0100
@@ -64,7 +64,7 @@
 by (auto simp: Gets_correct_def dest: nsp_has_no_Gets)
 
 lemma nsp_is_one_step [iff]: "one_step nsp"
-by (unfold one_step_def, clarify, ind_cases "ev#evs \<in> nsp" for ev evs, auto)
+  unfolding one_step_def by (clarify, ind_cases "ev#evs \<in> nsp" for ev evs, auto)
 
 lemma nsp_has_only_Says' [rule_format]: "evs \<in> nsp \<Longrightarrow>
 ev \<in> set evs \<longrightarrow> (\<exists>A B X. ev=Says A B X)"
isabelle