author | boehmes |
Mon, 17 Aug 2009 10:59:12 +0200 | |
changeset 32381 | 11542bebe4d4 |
parent 31849 | 431d8588bcad |
child 32479 | 521cc9bf2958 |
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 Commutative_Ring Enum List_Prefix Nat_Infinity Nested_Environment Option_ord Permutation Primes Product_ord SetsAndFunctions Tree While_Combinator Word "~~/src/HOL/ex/Commutative_Ring_Complete" "~~/src/HOL/ex/Records" begin (*avoid popular infixes*) code_reserved SML union inter upto end