src/HOL/String.thy
changeset 61076 bdc1e2f0a86a
parent 61032 b57df8eecad6
child 61348 d7215449be83
     1.1 --- a/src/HOL/String.thy	Tue Sep 01 17:25:36 2015 +0200
     1.2 +++ b/src/HOL/String.thy	Tue Sep 01 22:32:58 2015 +0200
     1.3 @@ -374,7 +374,7 @@
     1.4  
     1.5  definition size_literal :: "literal \<Rightarrow> nat"
     1.6  where
     1.7 -  [code]: "size_literal (s\<Colon>literal) = 0"
     1.8 +  [code]: "size_literal (s::literal) = 0"
     1.9  
    1.10  instance ..
    1.11