1.1 --- a/src/Tools/isac/Knowledge/RootEq.thy	Tue Aug 31 11:10:30 2010 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/RootEq.thy	Tue Aug 31 15:36:57 2010 +0200
     1.3 @@ -214,12 +214,12 @@
     1.4  
     1.5  val RootEq_erls =
     1.6       append_rls "RootEq_erls" Root_erls
     1.7 -          [Thm ("real_divide_divide2_eq",num_str real_divide_divide2_eq)
     1.8 +          [Thm ("divide_divide_eq_left",num_str @{thm divide_divide_eq_left})
     1.9             ];
    1.10  
    1.11  val RootEq_crls = 
    1.12       append_rls "RootEq_crls" Root_crls
    1.13 -          [Thm ("real_divide_divide2_eq",num_str real_divide_divide2_eq)
    1.14 +          [Thm ("divide_divide_eq_left",num_str @{thm divide_divide_eq_left})
    1.15             ];
    1.16  
    1.17  val rooteq_srls =