author | haftmann |
Fri, 30 Oct 2009 13:59:49 +0100 | |
changeset 33356 | 9157d0f9f00e |
parent 33042 | ddf1f03a9ad9 |
child 33500 | 22e5725be1f3 |
permissions | -rw-r--r-- |
(* Author: Florian Haftmann, TU Muenchen *) header {* A huge collection of equations to generate code from *} theory Codegenerator_Candidates imports Complex_Main AssocList Binomial Fset Enum List_Prefix Nat_Infinity Nested_Environment Option_ord Permutation "~~/src/HOL/Number_Theory/Primes" Product_ord SetsAndFunctions Tree While_Combinator Word "~~/src/HOL/Decision_Procs/Commutative_Ring_Complete" "~~/src/HOL/ex/Records" begin (*avoid popular infix*) code_reserved SML upto end