diff -r e67f05cc0ac5 -r fd7cd1edc18d src/HOL/ex/ExecutableContent.thy --- a/src/HOL/ex/ExecutableContent.thy Sat May 19 11:33:19 2007 +0200 +++ b/src/HOL/ex/ExecutableContent.thy Sat May 19 11:33:20 2007 +0200 @@ -14,7 +14,7 @@ Binomial Commutative_Ring "~~/src/HOL/ex/Commutative_Ring_Complete" -(* Executable_Real *) + Executable_Real GCD List_Prefix Nat_Infinity