--- a/src/ZF/Coind/Language.ML Tue Mar 07 13:21:38 1995 +0100
+++ b/src/ZF/Coind/Language.ML Tue Mar 07 13:27:09 1995 +0100
@@ -33,23 +33,3 @@
open Language;
-(* ############################################################ *)
-(* Inclusion in Quine Universes *)
-(* ############################################################ *)
-
-goal Language.thy "!!c.c:Const ==> c:quniv(A)";
-by (fast_tac (ZF_cs addIs [univ_subset_quniv RS subsetD,constU]) 1);
-qed "constQU";
-
-goal Language.thy "!!x.x:ExVar ==> x:quniv(A)";
-by (fast_tac (ZF_cs addIs [univ_subset_quniv RS subsetD,exvarU]) 1);
-qed "exvarQU";
-
-goal Language.thy "!!e.e:Exp ==> e:quniv(0)";
-by (rtac subsetD 1);
-by (rtac subset_trans 1);
-by (rtac Exp.dom_subset 1);
-by (rtac univ_subset_quniv 1);
-by (assume_tac 1);
-qed "expQU";
-