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