| changeset 24530 | 1bac25879117 |
| parent 24433 | 4a405457e9d6 |
| child 24626 | 85eceef2edc7 |
--- a/src/HOL/ex/ExecutableContent.thy Wed Sep 05 21:09:11 2007 +0200 +++ b/src/HOL/ex/ExecutableContent.thy Thu Sep 06 11:32:28 2007 +0200 @@ -13,8 +13,7 @@ Binomial Commutative_Ring "~~/src/HOL/ex/Commutative_Ring_Complete" - Executable_Rat - Executable_Real + "~~/src/HOL/Real/RealDef" GCD List_Prefix Nat_Infinity