# HG changeset patch
# User lcp
# Date 794579229 -3600
# Node ID c1e2004d07bd15bd32854887f4be790218a05f5e
# Parent  63f02d32509e21d7dcf260db570d99d08a811773
Deleted constQU, exvarQU, expQU by including Const,
ExpVar, Exp in Value.thy's codatatype declaration.

diff -r 63f02d32509e -r c1e2004d07bd src/ZF/Coind/Language.ML
--- 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";
-