src/HOL/ex/ExecutableContent.thy
author haftmann
Wed Mar 12 19:38:14 2008 +0100 (2008-03-12)
changeset 26265 4b63b9e9b10d
parent 26030 4ae4ea600e8f
child 26447 fef9dde61a46
permissions -rw-r--r--
separated Random.thy from Quickcheck.thy
haftmann@21917
     1
(*  ID:         $Id$
haftmann@21917
     2
    Author:     Florian Haftmann, TU Muenchen
haftmann@21917
     3
*)
haftmann@21917
     4
haftmann@21917
     5
header {* A huge set of executable constants *}
haftmann@21917
     6
haftmann@21917
     7
theory ExecutableContent
haftmann@21917
     8
imports
haftmann@21917
     9
  Main
haftmann@25536
    10
  Eval
haftmann@25963
    11
  Code_Index
haftmann@26030
    12
  "~~/src/HOL/ex/Records"
haftmann@21917
    13
  AssocList
haftmann@21917
    14
  Binomial
haftmann@21917
    15
  Commutative_Ring
haftmann@23690
    16
  "~~/src/HOL/ex/Commutative_Ring_Complete"
berghofe@24530
    17
  "~~/src/HOL/Real/RealDef"
haftmann@21917
    18
  GCD
haftmann@21917
    19
  List_Prefix
haftmann@21917
    20
  Nat_Infinity
haftmann@21917
    21
  NatPair
haftmann@24433
    22
  Nested_Environment
haftmann@21917
    23
  Permutation
haftmann@21917
    24
  Primes
haftmann@21917
    25
  Product_ord
haftmann@21917
    26
  SetsAndFunctions
haftmann@21917
    27
  State_Monad
haftmann@21917
    28
  While_Combinator
haftmann@21917
    29
  Word
haftmann@21917
    30
begin
haftmann@21917
    31
haftmann@26022
    32
lemma [code func, code func del]: "(Eval.term_of \<Colon> index \<Rightarrow> term) = Eval.term_of" ..
haftmann@25963
    33
declare fast_bv_to_nat_helper.simps [code func del]
haftmann@24197
    34
haftmann@21917
    35
end