src/HOL/Codegenerator_Test/Candidates.thy
author haftmann
Sun, 19 Feb 2012 15:30:35 +0100
changeset 46553 50a7e97fe653
parent 41884 335895ffbd94
child 49077 154f25a162e3
permissions -rw-r--r--
distributed lattice properties of predicates to places of instantiation


(* Author: Florian Haftmann, TU Muenchen *)

header {* A huge collection of equations to generate code from *}

theory Candidates
imports
  Complex_Main
  Library
  "~~/src/HOL/Library/List_Prefix"
  "~~/src/HOL/Number_Theory/Primes"
  "~~/src/HOL/ex/Records"
begin

inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
    empty: "sublist [] xs"
  | drop: "sublist ys xs \<Longrightarrow> sublist ys (x # xs)"
  | take: "sublist ys xs \<Longrightarrow> sublist (x # ys) (x # xs)"

code_pred sublist .

(*avoid popular infix*)
code_reserved SML upto

end