src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy
changeset 53361 1cb7d3c0cf31
parent 51599 1559e9266280
child 54295 45a5523d4a63
     1.1 --- a/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Sun Sep 01 14:00:05 2013 +0200
     1.2 +++ b/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Mon Sep 02 16:28:11 2013 +0200
     1.3 @@ -53,13 +53,6 @@
     1.4  (* If the compilation fails with an error "ambiguous implicit values",
     1.5     read \<section>7.1 in the Code Generation Manual *)
     1.6  
     1.7 -class ccpo_linorder = ccpo + linorder
     1.8 -
     1.9 -lemma [code]:
    1.10 -  "(Complete_Partial_Order.admissible :: ('a :: ccpo_linorder \<Rightarrow> bool) \<Rightarrow> bool) P = 
    1.11 -    (\<forall>A. Complete_Partial_Order.chain (op \<le>) A \<longrightarrow> (\<forall>x\<in>A. P x) \<longrightarrow> P (Sup A))"
    1.12 -unfolding admissible_def by blast
    1.13 -
    1.14  lemma [code]:
    1.15    "(gfp :: ('a :: complete_linorder \<Rightarrow> 'a) \<Rightarrow> 'a) f = Sup {u. u \<le> f u}"
    1.16  unfolding gfp_def by blast