src/HOL/ex/ExecutableContent.thy
author haftmann
Sat, 07 Mar 2009 10:06:31 +0100
changeset 30332 0d07f4823d3a
parent 30328 ab47f43f7581
child 30428 14f469e70eab
permissions -rw-r--r--
drop poisonous code equations

(*  Author:     Florian Haftmann, TU Muenchen
*)

header {* A huge set of executable constants *}

theory ExecutableContent
imports
  Complex_Main
  AssocList
  Binomial
  Commutative_Ring
  Enum
  List_Prefix
  Nat_Infinity
  Nested_Environment
  Option_ord
  Permutation
  Primes
  Product_ord
  SetsAndFunctions
  While_Combinator
  Word
  "~~/src/HOL/ex/Commutative_Ring_Complete"
  "~~/src/HOL/ex/Records"
begin

lemma [code, code del]:
  "(size :: 'a::size Predicate.pred => nat) = size" ..
lemma [code, code del]:
  "pred_size = pred_size" ..
lemma [code, code del]:
  "pred_case = pred_case" ..
lemma [code, code del]:
  "pred_rec = pred_rec" ..
lemma [code, code del]:
  "(Code_Eval.term_of \<Colon> 'a::{type, term_of} Predicate.pred \<Rightarrow> Code_Eval.term) = Code_Eval.term_of" ..
lemma [code, code del]:
  "(Code_Eval.term_of \<Colon> 'a::{type, term_of} Predicate.seq \<Rightarrow> Code_Eval.term) = Code_Eval.term_of" ..

text {* However, some aren't executable *}

declare pair_leq_def[code del]
declare max_weak_def[code del]
declare min_weak_def[code del]
declare ms_weak_def[code del]

end