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