src/HOL/Hyperreal/HTranscendental.thy
changeset 15077 89840837108e
parent 15013 34264f5e4691
child 15131 c69542757a4d
     1.1 --- a/src/HOL/Hyperreal/HTranscendental.thy	Mon Jul 26 15:48:50 2004 +0200
     1.2 +++ b/src/HOL/Hyperreal/HTranscendental.thy	Mon Jul 26 17:34:52 2004 +0200
     1.3 @@ -60,7 +60,7 @@
     1.4  
     1.5  lemma hypreal_sqrt_gt_zero_pow2: "0 < x ==> ( *f* sqrt) (x) ^ 2 = x"
     1.6  apply (cases x)
     1.7 -apply (auto intro: FreeUltrafilterNat_subset real_sqrt_gt_zero_pow2
     1.8 +apply (auto intro: FreeUltrafilterNat_subset 
     1.9              simp add: hypreal_less starfun hrealpow hypreal_zero_num 
    1.10              simp del: hpowr_Suc realpow_Suc)
    1.11  done