Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
"no_atp" fact that leads to unsound proofs in Sledgehammer
authorblanchet
Mon, 23 Aug 2010 14:21:57 +0200
changeset 38650 f22a564ac820
parent 38649 14c207135eff
child 38651 8aadda8e1338
"no_atp" fact that leads to unsound proofs in Sledgehammer
src/HOL/Orderings.thy file | annotate | diff | comparison | revisions 
--- 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)
isabelle