Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/ex/Codegenerator_Candidates.thy
author bulwahn
Wed, 21 Apr 2010 12:10:52 +0200
changeset 36253 6e969ce3dfcc
parent 36147 b43b22f63665
child 36962 5fb251d1c32f
permissions -rw-r--r--
added further inlining of boolean constants to the predicate compiler


(* 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
isabelle