src/HOL/Tools/Old_Datatype/old_datatype.ML
changeset 67091 1393c2340eec
parent 63352 4eaf35781b23
child 67318 0ee38196509e
     1.1 --- a/src/HOL/Tools/Old_Datatype/old_datatype.ML	Sun Nov 26 13:19:52 2017 +0100
     1.2 +++ b/src/HOL/Tools/Old_Datatype/old_datatype.ML	Sun Nov 26 21:08:32 2017 +0100
     1.3 @@ -47,7 +47,7 @@
     1.4  val Sumr_inject = @{thm Sumr_inject};
     1.5  
     1.6  val datatype_injI =
     1.7 -  @{lemma "(!!x. ALL y. f x = f y --> x = y) ==> inj f" by (simp add: inj_on_def)};
     1.8 +  @{lemma "(\<And>x. \<forall>y. f x = f y \<longrightarrow> x = y) \<Longrightarrow> inj f" by (simp add: inj_on_def)};
     1.9  
    1.10  
    1.11  (** proof of characteristic theorems **)