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
haftmann@31378
     1
haftmann@31378
     2
(* Author: Florian Haftmann, TU Muenchen *)
haftmann@21917
     3
haftmann@31378
     4
header {* A huge collection of equations to generate code from *}
haftmann@21917
     5
haftmann@37695
     6
theory Candidates
haftmann@21917
     7
imports
haftmann@27421
     8
  Complex_Main
haftmann@37695
     9
  Library
Christian@49077
    10
  "~~/src/HOL/Library/Sublist"
haftmann@32479
    11
  "~~/src/HOL/Number_Theory/Primes"
haftmann@35303
    12
  "~~/src/HOL/ex/Records"
haftmann@21917
    13
begin
haftmann@21917
    14
haftmann@33500
    15
inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
haftmann@33500
    16
    empty: "sublist [] xs"
haftmann@33500
    17
  | drop: "sublist ys xs \<Longrightarrow> sublist ys (x # xs)"
haftmann@33500
    18
  | take: "sublist ys xs \<Longrightarrow> sublist (x # ys) (x # xs)"
haftmann@33500
    19
haftmann@33500
    20
code_pred sublist .
haftmann@33500
    21
haftmann@33042
    22
(*avoid popular infix*)
haftmann@33042
    23
code_reserved SML upto
haftmann@31378
    24
haftmann@21917
    25
end