--- a/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy Sun Sep 01 14:00:05 2013 +0200
+++ b/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy Mon Sep 02 16:28:11 2013 +0200
@@ -53,13 +53,6 @@
(* If the compilation fails with an error "ambiguous implicit values",
read \<section>7.1 in the Code Generation Manual *)
-class ccpo_linorder = ccpo + linorder
-
-lemma [code]:
- "(Complete_Partial_Order.admissible :: ('a :: ccpo_linorder \<Rightarrow> bool) \<Rightarrow> bool) P =
- (\<forall>A. Complete_Partial_Order.chain (op \<le>) A \<longrightarrow> (\<forall>x\<in>A. P x) \<longrightarrow> P (Sup A))"
-unfolding admissible_def by blast
-
lemma [code]:
"(gfp :: ('a :: complete_linorder \<Rightarrow> 'a) \<Rightarrow> 'a) f = Sup {u. u \<le> f u}"
unfolding gfp_def by blast