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