1.1 --- a/src/HOL/ex/Codegenerator_Candidates.thy	Fri Jul 02 14:23:17 2010 +0200
     1.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.3 @@ -1,39 +0,0 @@
     1.4 -
     1.5 -(* Author: Florian Haftmann, TU Muenchen *)
     1.6 -
     1.7 -header {* A huge collection of equations to generate code from *}
     1.8 -
     1.9 -theory Codegenerator_Candidates
    1.10 -imports
    1.11 -  Complex_Main
    1.12 -  AssocList
    1.13 -  Binomial
    1.14 -  "~~/src/HOL/Decision_Procs/Commutative_Ring_Complete"
    1.15 -  Dlist
    1.16 -  Fset
    1.17 -  Enum
    1.18 -  List_Prefix
    1.19 -  More_List
    1.20 -  Nat_Infinity
    1.21 -  Nested_Environment
    1.22 -  Option_ord
    1.23 -  Permutation
    1.24 -  "~~/src/HOL/Number_Theory/Primes"
    1.25 -  Product_ord
    1.26 -  "~~/src/HOL/ex/Records"
    1.27 -  RBT
    1.28 -  SetsAndFunctions
    1.29 -  While_Combinator
    1.30 -begin
    1.31 -
    1.32 -inductive sublist :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool" where
    1.33 -    empty: "sublist [] xs"
    1.34 -  | drop: "sublist ys xs \<Longrightarrow> sublist ys (x # xs)"
    1.35 -  | take: "sublist ys xs \<Longrightarrow> sublist (x # ys) (x # xs)"
    1.36 -
    1.37 -code_pred sublist .
    1.38 -
    1.39 -(*avoid popular infix*)
    1.40 -code_reserved SML upto
    1.41 -
    1.42 -end