src/HOL/Library/Perm.thy
changeset 64911 f0e07600de47
parent 63993 9c0ff0c12116
child 67399 eab6ce8368fa
     1.1 --- a/src/HOL/Library/Perm.thy	Tue Jan 17 11:26:21 2017 +0100
     1.2 +++ b/src/HOL/Library/Perm.thy	Tue Jan 17 13:59:10 2017 +0100
     1.3 @@ -12,7 +12,7 @@
     1.4    Grieviously missing are cycles since these would require more
     1.5    elaboration, e.g. the concept of distinct lists equivalent
     1.6    under rotation, which maybe would also deserve its own theory.
     1.7 -  But see theory @{text "src/HOL/ex/Perm_Fragments.thy"} for
     1.8 +  But see theory \<open>src/HOL/ex/Perm_Fragments.thy\<close> for
     1.9    fragments on that.
    1.10  \<close>
    1.11