src/HOL/Typedef.thy
changeset 61799 4cf66f21b764
parent 61102 0ec9fd8d8119
child 63434 c956d995bec6
     1.1 --- a/src/HOL/Typedef.thy	Mon Dec 07 10:23:50 2015 +0100
     1.2 +++ b/src/HOL/Typedef.thy	Mon Dec 07 10:38:04 2015 +0100
     1.3 @@ -14,7 +14,7 @@
     1.4    assumes Rep: "Rep x \<in> A"
     1.5      and Rep_inverse: "Abs (Rep x) = x"
     1.6      and Abs_inverse: "y \<in> A \<Longrightarrow> Rep (Abs y) = y"
     1.7 -  -- \<open>This will be axiomatized for each typedef!\<close>
     1.8 +  \<comment> \<open>This will be axiomatized for each typedef!\<close>
     1.9  begin
    1.10  
    1.11  lemma Rep_inject: "Rep x = Rep y \<longleftrightarrow> x = y"