src/HOL/Orderings.thy
changeset 38786 e46e7a9cb622
parent 38715 6513ea67d95d
child 38795 848be46708dc
     1.1 --- a/src/HOL/Orderings.thy	Thu Aug 26 13:44:50 2010 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Thu Aug 26 20:51:17 2010 +0200
     1.3 @@ -640,7 +640,7 @@
     1.4  let
     1.5    val All_binder = Syntax.binder_name @{const_syntax All};
     1.6    val Ex_binder = Syntax.binder_name @{const_syntax Ex};
     1.7 -  val impl = @{const_syntax "op -->"};
     1.8 +  val impl = @{const_syntax HOL.implies};
     1.9    val conj = @{const_syntax "op &"};
    1.10    val less = @{const_syntax less};
    1.11    val less_eq = @{const_syntax less_eq};