src/HOL/Codegenerator_Test/Candidates.thy
author Christian Sternagel
Thu Aug 30 15:44:03 2012 +0900 (2012-08-30)
changeset 49093 fdc301f592c4
parent 49077 154f25a162e3
child 51160 599ff65b85e2
permissions -rw-r--r--
forgot to add lemmas
     1 
     2 (* Author: Florian Haftmann, TU Muenchen *)
     3 
     4 header {* A huge collection of equations to generate code from *}
     5 
     6 theory Candidates
     7 imports
     8   Complex_Main
     9   Library
    10   "~~/src/HOL/Library/Sublist"
    11   "~~/src/HOL/Number_Theory/Primes"
    12   "~~/src/HOL/ex/Records"
    13 begin
    14 
    15 inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
    16     empty: "sublist [] xs"
    17   | drop: "sublist ys xs \<Longrightarrow> sublist ys (x # xs)"
    18   | take: "sublist ys xs \<Longrightarrow> sublist (x # ys) (x # xs)"
    19 
    20 code_pred sublist .
    21 
    22 (*avoid popular infix*)
    23 code_reserved SML upto
    24 
    25 end