replaced generic 'hide' command by more conventional 'hide_class', 'hide_type', 'hide_const', 'hide_fact' -- frees some popular keywords;
(* Author: Florian Haftmann, TU Muenchen *)
header {* A huge collection of equations to generate code from *}
theory Codegenerator_Candidates
imports
Complex_Main
AssocList
Binomial
"~~/src/HOL/Decision_Procs/Commutative_Ring_Complete"
Dlist
Fset
Enum
List_Prefix
Nat_Infinity
Nested_Environment
Option_ord
Permutation
"~~/src/HOL/Number_Theory/Primes"
Product_ord
"~~/src/HOL/ex/Records"
RBT
SetsAndFunctions
While_Combinator
Word
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