src/HOL/ex/ExecutableContent.thy
author nipkow
Fri Mar 06 17:38:47 2009 +0100 (2009-03-06)
changeset 30313 b2441b0c8d38
parent 29125 d41182a8135c
child 30328 ab47f43f7581
permissions -rw-r--r--
added lemmas
     1 (*  Author:     Florian Haftmann, TU Muenchen
     2 *)
     3 
     4 header {* A huge set of executable constants *}
     5 
     6 theory ExecutableContent
     7 imports
     8   Complex_Main
     9   AssocList
    10   Binomial
    11   Commutative_Ring
    12   Enum
    13   List_Prefix
    14   Nat_Infinity
    15   Nested_Environment
    16   Option_ord
    17   Permutation
    18   Primes
    19   Product_ord
    20   SetsAndFunctions
    21   While_Combinator
    22   Word
    23   "~~/src/HOL/ex/Commutative_Ring_Complete"
    24   "~~/src/HOL/ex/Records"
    25 begin
    26 
    27 text {* However, some aren't executable *}
    28 
    29 declare pair_leq_def[code del]
    30 declare max_weak_def[code del]
    31 declare min_weak_def[code del]
    32 declare ms_weak_def[code del]
    33 
    34 end