src/HOL/Orderings.thy
changeset 38650 f22a564ac820
parent 37767 a2b7a20d6ea3
child 38705 aaee86c0e237
     1.1 --- a/src/HOL/Orderings.thy	Mon Aug 23 12:13:58 2010 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Mon Aug 23 14:21:57 2010 +0200
     1.3 @@ -1264,7 +1264,8 @@
     1.4  begin
     1.5  
     1.6  definition
     1.7 -  top_fun_eq: "top = (\<lambda>x. top)"
     1.8 +  top_fun_eq [no_atp]: "top = (\<lambda>x. top)"
     1.9 +declare top_fun_eq_raw [no_atp]
    1.10  
    1.11  instance proof
    1.12  qed (simp add: top_fun_eq le_fun_def)