| author | hoelzl |
| Mon, 15 Jun 2009 12:14:40 +0200 | |
| changeset 31809 | 06372924e86c |
| parent 31807 | 039893a9a77d |
| child 31849 | 431d8588bcad |
| 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 Code_Set 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