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