# HG changeset patch
# User huffman
# Date 1166126619 -3600
# Node ID bf253f7075b481b26d68c153863b71f3900407fc
# Parent  a2e7a79159e40ca8f9e552e572db7dd30e75523d
remove usage of ultra tactic

diff -r a2e7a79159e4 -r bf253f7075b4 src/HOL/Hyperreal/Star.thy
--- a/src/HOL/Hyperreal/Star.thy	Thu Dec 14 19:29:48 2006 +0100
+++ b/src/HOL/Hyperreal/Star.thy	Thu Dec 14 21:03:39 2006 +0100
@@ -204,7 +204,9 @@
 apply (rule_tac x = x in star_cases)
 apply (drule_tac x = x in spec)
 apply (drule_tac x = "( *f* f) x" in spec)
-apply (auto dest!: FreeUltrafilterNat_Compl_mem simp add: starfun, ultra)
+apply (auto simp add: starfun_star_n)
+apply (simp add: star_n_eq_iff [symmetric])
+apply (simp add: starfun_star_n [of f, symmetric])
 done
 
 lemma is_starext_starfun_iff: "(is_starext F f) = (F = *f* f)"