src/HOL/Library/Permutation.thy
changeset 61585 a9599d3d7610
parent 60515 484559628038
child 61699 a81dc5c4d6a9
--- a/src/HOL/Library/Permutation.thy	Thu Nov 05 10:35:37 2015 +0100
+++ b/src/HOL/Library/Permutation.thy	Thu Nov 05 10:39:49 2015 +0100
@@ -116,7 +116,7 @@
   apply (safe intro!: perm_append2)
   apply (rule append_perm_imp_perm)
   apply (rule perm_append_swap [THEN perm.trans])
-    -- \<open>the previous step helps this @{text blast} call succeed quickly\<close>
+    \<comment> \<open>the previous step helps this \<open>blast\<close> call succeed quickly\<close>
   apply (blast intro: perm_append_swap)
   done