src/HOL/Library/OptionalSugar.thy
changeset 56245 84fc7dfa3cd4
parent 55052 c602013f127e
child 61143 5f898411ce87
     1.1 --- a/src/HOL/Library/OptionalSugar.thy	Fri Mar 21 15:12:03 2014 +0100
     1.2 +++ b/src/HOL/Library/OptionalSugar.thy	Fri Mar 21 20:33:56 2014 +0100
     1.3 @@ -33,7 +33,7 @@
     1.4  (* aligning equations *)
     1.5  notation (tab output)
     1.6    "HOL.eq"  ("(_) \<^raw:}\putisatab\isa{\ >=\<^raw:}\putisatab\isa{> (_)" [50,49] 50) and
     1.7 -  "=="  ("(_) \<^raw:}\putisatab\isa{\ >\<equiv>\<^raw:}\putisatab\isa{> (_)")
     1.8 +  "Pure.eq"  ("(_) \<^raw:}\putisatab\isa{\ >\<equiv>\<^raw:}\putisatab\isa{> (_)")
     1.9  
    1.10  (* Let *)
    1.11  translations