src/HOL/Orderings.thy
changeset 38795 848be46708dc
parent 38786 e46e7a9cb622
child 41075 4bed56dc95fb
     1.1 --- a/src/HOL/Orderings.thy	Fri Aug 27 10:55:20 2010 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Fri Aug 27 10:56:46 2010 +0200
     1.3 @@ -641,7 +641,7 @@
     1.4    val All_binder = Syntax.binder_name @{const_syntax All};
     1.5    val Ex_binder = Syntax.binder_name @{const_syntax Ex};
     1.6    val impl = @{const_syntax HOL.implies};
     1.7 -  val conj = @{const_syntax "op &"};
     1.8 +  val conj = @{const_syntax HOL.conj};
     1.9    val less = @{const_syntax less};
    1.10    val less_eq = @{const_syntax less_eq};
    1.11