src/HOL/Set.thy
changeset 38786 e46e7a9cb622
parent 38715 6513ea67d95d
child 38795 848be46708dc
     1.1 --- a/src/HOL/Set.thy	Thu Aug 26 13:44:50 2010 +0200
     1.2 +++ b/src/HOL/Set.thy	Thu Aug 26 20:51:17 2010 +0200
     1.3 @@ -219,7 +219,7 @@
     1.4    val Type (set_type, _) = @{typ "'a set"};   (* FIXME 'a => bool (!?!) *)
     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 sbset = @{const_syntax subset};
    1.11    val sbset_eq = @{const_syntax subset_eq};