src/HOL/Real/RealDef.thy
changeset 24075 366d4d234814
parent 23879 4776af8be741
child 24198 4031da6d8ba3
     1.1 --- a/src/HOL/Real/RealDef.thy	Mon Jul 30 19:46:15 2007 +0200
     1.2 +++ b/src/HOL/Real/RealDef.thy	Tue Jul 31 00:56:26 2007 +0200
     1.3 @@ -832,8 +832,7 @@
     1.4   
     1.5  
     1.6  use "real_arith.ML"
     1.7 -
     1.8 -setup real_arith_setup
     1.9 +declaration {* K real_arith_setup *}
    1.10  
    1.11  
    1.12  subsection{* Simprules combining x+y and 0: ARE THEY NEEDED?*}