haftmann@31378: haftmann@31378: (* Author: Florian Haftmann, TU Muenchen *) haftmann@21917: wenzelm@58889: section {* A huge collection of equations to generate code from *} haftmann@21917: haftmann@37695: theory Candidates haftmann@21917: imports haftmann@27421: Complex_Main haftmann@51160: "~~/src/HOL/Library/Library" haftmann@51161: "~~/src/HOL/Library/Sublist_Order" haftmann@51173: "~~/src/HOL/Number_Theory/Eratosthenes" haftmann@35303: "~~/src/HOL/ex/Records" haftmann@21917: begin haftmann@21917: haftmann@51161: inductive sublist :: "'a list \ 'a list \ bool" haftmann@51161: where haftmann@51161: empty: "sublist [] xs" haftmann@51161: | drop: "sublist ys xs \ sublist ys (x # xs)" haftmann@51161: | take: "sublist ys xs \ sublist (x # ys) (x # xs)" haftmann@33500: haftmann@33500: code_pred sublist . haftmann@33500: haftmann@51161: code_reserved SML upto -- {* avoid popular infix *} haftmann@31378: haftmann@21917: end