author | haftmann |
Mon, 29 Jun 2009 12:18:55 +0200 | |
changeset 31849 | 431d8588bcad |
parent 31807 | 039893a9a77d |
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