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/Extensions.thy
changeset 76289 a6cc15ec45b2
parent 76288 b82ac7ef65ec 
--- a/src/HOL/Auth/Guard/Extensions.thy	Thu Oct 13 15:49:09 2022 +0100
+++ b/src/HOL/Auth/Guard/Extensions.thy	Thu Oct 13 16:00:22 2022 +0100
@@ -306,7 +306,7 @@
 "one_step p == \<forall>evs ev. ev#evs \<in> p \<longrightarrow> evs \<in> p"
 
 lemma one_step_Cons [dest]: "\<lbrakk>one_step p; ev#evs \<in> p\<rbrakk> \<Longrightarrow> evs \<in> p"
-  unfolding one_step_def by (blast)
+  unfolding one_step_def by blast
 
 lemma one_step_app: "\<lbrakk>evs@evs' \<in> p; one_step p; [] \<in> p\<rbrakk> \<Longrightarrow> evs' \<in> p"
 by (induct evs, auto)
@@ -320,7 +320,7 @@
 
 lemma has_only_SaysD: "\<lbrakk>ev \<in> set evs; evs \<in> p; has_only_Says p\<rbrakk>
 \<Longrightarrow> \<exists>A B X. ev = Says A B X"
-  unfolding has_only_Says_def by (blast)
+  unfolding has_only_Says_def by blast
 
 lemma in_has_only_Says [dest]: "\<lbrakk>has_only_Says p; evs \<in> p; ev \<in> set evs\<rbrakk>
 \<Longrightarrow> \<exists>A B X. ev = Says A B X"
isabelle