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