# HG changeset patch
# User berghofe
# Date 1034252357 -7200
# Node ID fdf7e9388be73d3786eeacb1c3847245720f27f7
# Parent  c41e88151b54198f261546839caa9b10fe674cf9
Removed obsolete function "Funs".

diff -r c41e88151b54 -r fdf7e9388be7 src/HOL/Datatype_Universe.ML
--- a/src/HOL/Datatype_Universe.ML	Thu Oct 10 14:18:01 2002 +0200
+++ b/src/HOL/Datatype_Universe.ML	Thu Oct 10 14:19:17 2002 +0200
@@ -382,43 +382,6 @@
 by (blast_tac (claset() addSEs [Push_Node_inject]) 1);
 qed "Lim_inject";
 
-Goalw [Funs_def] "S <= T ==> Funs S <= Funs T";
-by (Blast_tac 1);
-qed "Funs_mono";
-
-val [prem] = Goalw [Funs_def] "(!!x. f x : S) ==> f : Funs S";
-by (blast_tac (claset() addIs [prem]) 1);
-qed "FunsI";
-
-Goalw [Funs_def] "f : Funs S ==> f x : S";
-by (etac CollectE 1);
-by (etac subsetD 1);
-by (rtac rangeI 1);
-qed "FunsD";
-
-val [p1, p2] = Goalw [o_def]
-   "[| f : Funs R; !!x. x : R ==> r (a x) = x |] ==> r o (a o f) = f";
-by (rtac (p2 RS ext) 1);
-by (rtac (p1 RS FunsD) 1);
-qed "Funs_inv";
-
-val [p1, p2, p3] = Goalw [o_def]
-     "[| inj g; f : Funs (range g); !!h. f = g o h ==> P |] ==> P";
-by (res_inst_tac [("h", "%x. THE y. (f::'c=>'b) x = g y")] p3 1);
-by (rtac ext 1);
-by (rtac (p2 RS FunsD RS rangeE) 1);
-by (rtac theI 1);
-by (atac 1);
-by (rtac (p1 RS injD) 1);
-by (etac (sym RS trans) 1);
-by (atac 1);
-qed "Funs_rangeE";
-
-Goal "a : S ==> (%x. a) : Funs S";
-by (rtac FunsI 1);
-by (assume_tac 1);
-qed "Funs_nonempty";
-
 
 (*** proving equality of sets and functions using ntrunc ***)
 
diff -r c41e88151b54 -r fdf7e9388be7 src/HOL/Datatype_Universe.thy
--- a/src/HOL/Datatype_Universe.thy	Thu Oct 10 14:18:01 2002 +0200
+++ b/src/HOL/Datatype_Universe.thy	Thu Oct 10 14:19:17 2002 +0200
@@ -33,9 +33,7 @@
   Numb      :: nat => ('a, 'b) dtree
   Scons     :: [('a, 'b) dtree, ('a, 'b) dtree] => ('a, 'b) dtree
   In0,In1   :: ('a, 'b) dtree => ('a, 'b) dtree
-
   Lim       :: ('b => ('a, 'b) dtree) => ('a, 'b) dtree
-  Funs      :: "'u set => ('t => 'u) set"
 
   ntrunc    :: [nat, ('a, 'b) dtree] => ('a, 'b) dtree
 
@@ -75,7 +73,6 @@
 
   (*Function spaces*)
   Lim_def "Lim f == Union {z. ? x. z = Push_Node (Inl x) ` (f x)}"
-  Funs_def "Funs S == {f. range f <= S}"
 
   (*the set of nodes with depth less than k*)
   ndepth_def "ndepth(n) == (%(f,x). LEAST k. f k = Inr 0) (Rep_Node n)"