# HG changeset patch
# User huffman
# Date 1166131179 -3600
# Node ID f9d085c2625c0b3bac7c53f24040105bf95f42a4
# Parent  f44628fb2033398d5773be3ed0253bb54f0b6328
remove Hyperreal/fuf.ML

diff -r f44628fb2033 -r f9d085c2625c src/HOL/Hyperreal/fuf.ML
--- a/src/HOL/Hyperreal/fuf.ML	Thu Dec 14 22:18:08 2006 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,75 +0,0 @@
-(*  Title       : HOL/Hyperreal/fuf.ML
-    ID          : $Id$
-    Author      : Jacques D. Fleuriot
-    Copyright   : 1998  University of Cambridge
-                  1999  University of Edinburgh
-
-Simple tactics to help proofs involving our free ultrafilter
-(FreeUltrafilterNat). We rely on the fact that filters satisfy the
-finite intersection property.
-*)
-
-val FreeUltrafilterNat_empty = thm "FreeUltrafilterNat_empty";
-val FreeUltrafilterNat_subset = thm "FreeUltrafilterNat_subset";
-val FreeUltrafilterNat_Compl_mem = thm "FreeUltrafilterNat_Compl_mem";
-val FreeUltrafilterNat_Int = thm "FreeUltrafilterNat_Int";
-
-local
-
-exception FUFempty;
-
-fun get_fuf_hyps [] zs = zs
-|   get_fuf_hyps (x::xs) zs =
-        case (concl_of x) of
-        (_ $ (Const ("Not",_) $ (Const ("op :",_) $ _ $
-             Const ("StarDef.FreeUltrafilterNat",_)))) =>  get_fuf_hyps xs
-                                              ((x RS FreeUltrafilterNat_Compl_mem)::zs)
-       |(_ $ (Const ("op :",_) $ _ $
-             Const ("StarDef.FreeUltrafilterNat",_)))  =>  get_fuf_hyps xs (x::zs)
-       | _ => get_fuf_hyps xs zs;
-
-fun inter_prems [] = raise FUFempty
-|   inter_prems [x] = x
-|   inter_prems (x::y::ys) =
-      inter_prems (([x,y] MRS FreeUltrafilterNat_Int) :: ys);
-
-in
-
-(*---------------------------------------------------------------
-   solves goals of the form
-    [| A1: FUF; A2: FUF; ...; An: FUF |] ==> B : FUF
-   where A1 Int A2 Int ... Int An <= B
- ---------------------------------------------------------------*)
-
-fun fuf_tac css i = METAHYPS(fn prems =>
-                    (rtac ((inter_prems (get_fuf_hyps prems [])) RS
-                           FreeUltrafilterNat_subset) 1) THEN
-                    auto_tac css) i;
-
-fun Fuf_tac i = fuf_tac (clasimpset ()) i;
-
-
-(*---------------------------------------------------------------
-   solves goals of the form
-    [| A1: FUF; A2: FUF; ...; An: FUF |] ==> P
-   where A1 Int A2 Int ... Int An <= {} since {} ~: FUF
-   (i.e. uses fact that FUF is a proper filter)
- ---------------------------------------------------------------*)
-
-fun fuf_empty_tac css i = METAHYPS (fn prems =>
-  rtac ((inter_prems (get_fuf_hyps prems [])) RS
-    (FreeUltrafilterNat_subset RS (FreeUltrafilterNat_empty RS notE))) 1
-                     THEN auto_tac css) i;
-
-fun Fuf_empty_tac i = fuf_empty_tac (clasimpset ()) i;
-
-
-(*---------------------------------------------------------------
-   In fact could make this the only tactic: just need to
-   use contraposition and then look for empty set.
- ---------------------------------------------------------------*)
-
-fun ultra_tac css i = rtac ccontr i THEN fuf_empty_tac css i;
-fun Ultra_tac i = ultra_tac (clasimpset ()) i;
-
-end;
diff -r f44628fb2033 -r f9d085c2625c src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Thu Dec 14 22:18:08 2006 +0100
+++ b/src/HOL/IsaMakefile	Thu Dec 14 22:19:39 2006 +0100
@@ -170,7 +170,7 @@
   Hyperreal/NSA.thy Hyperreal/NthRoot.thy Hyperreal/Poly.thy			\
   Hyperreal/SEQ.thy Hyperreal/Series.thy Hyperreal/Star.thy			\
   Hyperreal/Taylor.thy Hyperreal/FrechetDeriv.thy Hyperreal/Deriv.thy		\
-  Hyperreal/Transcendental.thy Hyperreal/fuf.ML Hyperreal/hypreal_arith.ML	\
+  Hyperreal/Transcendental.thy Hyperreal/hypreal_arith.ML			\
   Complex/Complex_Main.thy Complex/CLim.thy Complex/CSeries.thy			\
   Complex/CStar.thy Complex/Complex.thy Complex/ComplexBin.thy			\
   Complex/NSCA.thy Complex/NSComplex.thy Complex/document/root.tex 		\