src/HOL/Real.thy
changeset 48891 c0eafbd55de3
parent 36899 bcd6fce5bf06
child 51521 36fa825e0ea7
child 51539 625d2ec0bbff
     1.1 --- a/src/HOL/Real.thy	Wed Aug 22 22:47:16 2012 +0200
     1.2 +++ b/src/HOL/Real.thy	Wed Aug 22 22:55:41 2012 +0200
     1.3 @@ -1,8 +1,8 @@
     1.4  theory Real
     1.5  imports RComplete RealVector
     1.6 -uses "Tools/SMT/smt_real.ML"
     1.7  begin
     1.8  
     1.9 -setup {* SMT_Real.setup *}
    1.10 +ML_file "Tools/SMT/smt_real.ML"
    1.11 +setup SMT_Real.setup
    1.12  
    1.13  end