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
haftmann@28952
     1
(*  Author:     Florian Haftmann, TU Muenchen
haftmann@21917
     2
*)
haftmann@21917
     3
haftmann@21917
     4
header {* A huge set of executable constants *}
haftmann@21917
     5
haftmann@21917
     6
theory ExecutableContent
haftmann@21917
     7
imports
haftmann@27421
     8
  Complex_Main
haftmann@21917
     9
  AssocList
haftmann@21917
    10
  Binomial
haftmann@21917
    11
  Commutative_Ring
haftmann@27421
    12
  Enum
haftmann@21917
    13
  List_Prefix
haftmann@21917
    14
  Nat_Infinity
haftmann@24433
    15
  Nested_Environment
haftmann@26515
    16
  Option_ord
haftmann@21917
    17
  Permutation
haftmann@21917
    18
  Primes
haftmann@21917
    19
  Product_ord
haftmann@21917
    20
  SetsAndFunctions
haftmann@21917
    21
  While_Combinator
haftmann@21917
    22
  Word
haftmann@27421
    23
  "~~/src/HOL/ex/Commutative_Ring_Complete"
haftmann@27421
    24
  "~~/src/HOL/ex/Records"
haftmann@21917
    25
begin
haftmann@21917
    26
krauss@29125
    27
text {* However, some aren't executable *}
krauss@29125
    28
krauss@29125
    29
declare pair_leq_def[code del]
krauss@29125
    30
declare max_weak_def[code del]
krauss@29125
    31
declare min_weak_def[code del]
krauss@29125
    32
declare ms_weak_def[code del]
krauss@29125
    33
haftmann@21917
    34
end