# HG changeset patch
# User blanchet
# Date 1282566117 -7200
# Node ID f22a564ac8204b6c319ee21bbbc4cb09daf6171c
# Parent  14c207135effab872bc10badce8bfc2c9a5e6758
"no_atp" fact that leads to unsound proofs in Sledgehammer

diff -r 14c207135eff -r f22a564ac820 src/HOL/Orderings.thy
--- 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)