src/HOL/Codegenerator_Test/Candidates.thy
changeset 37695 71e84a203c19
parent 37407 61dd8c145da7
child 41884 335895ffbd94
equal deleted inserted replaced
37694:19e8b730ddeb 37695:71e84a203c19
       
     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   List_Prefix
       
    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