src/HOL/Codegenerator_Test/Candidates.thy
author wenzelm
Sun Nov 02 18:21:45 2014 +0100 (2014-11-02)
changeset 58889 5b7a9633cfa8
parent 58740 cb9d84d3e7f2
child 59484 a130ae7a9398
permissions -rw-r--r--
modernized header uniformly as section;
haftmann@31378
     1
haftmann@31378
     2
(* Author: Florian Haftmann, TU Muenchen *)
haftmann@21917
     3
wenzelm@58889
     4
section {* 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@51160
     9
  "~~/src/HOL/Library/Library"
haftmann@51161
    10
  "~~/src/HOL/Library/Sublist_Order"
haftmann@51173
    11
  "~~/src/HOL/Number_Theory/Eratosthenes"
haftmann@35303
    12
  "~~/src/HOL/ex/Records"
haftmann@21917
    13
begin
haftmann@21917
    14
haftmann@51161
    15
inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"
haftmann@51161
    16
where
haftmann@51161
    17
  empty: "sublist [] xs"
haftmann@51161
    18
| drop: "sublist ys xs \<Longrightarrow> sublist ys (x # xs)"
haftmann@51161
    19
| take: "sublist ys xs \<Longrightarrow> sublist (x # ys) (x # xs)"
haftmann@33500
    20
haftmann@33500
    21
code_pred sublist .
haftmann@33500
    22
haftmann@51161
    23
code_reserved SML upto -- {* avoid popular infix *}
haftmann@31378
    24
haftmann@21917
    25
end