# HG changeset patch
# User paulson
# Date 834747662 -7200
# Node ID e2b7ba2160f12994c32ed7790cf0cafe07d7b0c5
# Parent  09fff2f0d727de96715d1b411ba1aa75879eaf6a
Obsolete relics concerned with recursion

diff -r 09fff2f0d727 -r e2b7ba2160f1 src/HOL/ex/Rec.ML
--- a/src/HOL/ex/Rec.ML	Thu Jun 13 16:22:37 1996 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,5 +0,0 @@
-open Rec;
-
-goalw thy [mono_def,Domf_def] "mono(Domf(F))";
-by (DEPTH_SOLVE (slow_step_tac set_cs 1));
-qed "mono_Domf";
diff -r 09fff2f0d727 -r e2b7ba2160f1 src/HOL/ex/Rec.thy
--- a/src/HOL/ex/Rec.thy	Thu Jun 13 16:22:37 1996 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,9 +0,0 @@
-Rec = Fixedpt +
-consts
-fix     :: ('a=>'a) => 'a
-Dom     :: (('a=>'b) => ('a=>'b)) => 'a set
-Domf    :: (('a=>'b) => ('a=>'b)) => 'a set => 'a set
-rules
-Domf_def "Domf(F,D) == {y . !f g. (!x:D. f(x)=g(x)) --> F(f,y)=F(g,y)}"
-Dom_def  "Dom(F) == lfp(Domf(F))"
-end