# HG changeset patch
# User paulson
# Date 939631971 -7200
# Node ID 1be9b63e7d93e70910d56160c5d65ef804f711b9
# Parent  1a85ba81d01945b20d40d9e439ca82a825cb5023
replaced {x. True} by UNIV to work with the new simprule, Collect_const

diff -r 1a85ba81d019 -r 1be9b63e7d93 src/HOL/Induct/LList.ML
--- a/src/HOL/Induct/LList.ML	Mon Oct 11 10:51:24 1999 +0200
+++ b/src/HOL/Induct/LList.ML	Mon Oct 11 10:52:51 1999 +0200
@@ -108,7 +108,7 @@
 
 (*A typical use of co-induction to show membership in the gfp. 
   Bisimulation is  range(%x. LList_corec x f) *)
-Goal "LList_corec a f : llist({u. True})";
+Goal "LList_corec a f : llist UNIV";
 by (res_inst_tac [("X", "range(%x. LList_corec x ?g)")] llist_coinduct 1);
 by (rtac rangeI 1);
 by Safe_tac;
@@ -247,14 +247,14 @@
 \ ==> h1=h2";
 by (rtac ext 1);
 (*next step avoids an unknown (and flexflex pair) in simplification*)
-by (res_inst_tac [("A", "{u. True}"),
+by (res_inst_tac [("A", "UNIV"),
                   ("r", "range(%u. (h1(u),h2(u)))")] LList_equalityI 1);
 by (rtac rangeI 1);
 by Safe_tac;
 by (stac prem1 1);
 by (stac prem2 1);
 by (simp_tac (simpset() addsimps [LListD_Fun_NIL_I,
-				  CollectI RS LListD_Fun_CONS_I]) 1);
+				  UNIV_I RS LListD_Fun_CONS_I]) 1);
 qed "LList_corec_unique";
 
 val [prem] = 
diff -r 1a85ba81d019 -r 1be9b63e7d93 src/HOL/Real/Hyperreal/HyperDef.ML
--- a/src/HOL/Real/Hyperreal/HyperDef.ML	Mon Oct 11 10:51:24 1999 +0200
+++ b/src/HOL/Real/Hyperreal/HyperDef.ML	Mon Oct 11 10:52:51 1999 +0200
@@ -1848,7 +1848,7 @@
 Goal "inj hypreal_of_nat";
 by (rtac injI 1);
 by (auto_tac (claset() addSDs [FreeUltrafilterNat_P],
-        simpset() addsimps [hypreal_of_nat_iff,
+        simpset() addsimps [split_if_mem1, hypreal_of_nat_iff,
         real_add_right_cancel,inj_real_of_nat RS injD]));
 qed "inj_hypreal_of_nat";
 
diff -r 1a85ba81d019 -r 1be9b63e7d93 src/HOL/Real/PRat.ML
--- a/src/HOL/Real/PRat.ML	Mon Oct 11 10:51:24 1999 +0200
+++ b/src/HOL/Real/PRat.ML	Mon Oct 11 10:52:51 1999 +0200
@@ -786,22 +786,22 @@
 by (auto_tac (claset(),simpset() addsimps [prat_less_not_refl]));
 qed "lemma_prat_less_1_not_memEx";
 
-Goal "{x::prat. x < prat_of_pnat (Abs_pnat 1)} ~= {q::prat. True}";
+Goal "{x::prat. x < prat_of_pnat (Abs_pnat 1)} ~= UNIV";
 by (rtac notI 1);
 by (cut_facts_tac [lemma_prat_less_1_not_memEx] 1);
 by (Asm_full_simp_tac 1);
 qed "lemma_prat_less_1_set_not_rat_set";
 
 Goalw [psubset_def,subset_def] 
-      "{x::prat. x < prat_of_pnat (Abs_pnat 1)} < {q::prat. True}";
-by (asm_full_simp_tac (simpset() addsimps 
-      [lemma_prat_less_1_set_not_rat_set,
-       lemma_prat_less_1_not_memEx]) 1);
+      "{x::prat. x < prat_of_pnat (Abs_pnat 1)} < UNIV";
+by (asm_full_simp_tac
+    (simpset() addsimps [lemma_prat_less_1_set_not_rat_set,
+			 lemma_prat_less_1_not_memEx]) 1);
 qed "lemma_prat_less_1_set_psubset_rat_set";
 
 (*** prove non_emptiness of type ***)
 Goal "{x::prat. x < prat_of_pnat (Abs_pnat 1)} : {A. {} < A & \
-\               A < {q::prat. True} & \
+\               A < UNIV & \
 \               (!y: A. ((!z. z < y --> z: A) & \
 \               (? u: A. y < u)))}";
 by (auto_tac (claset() addDs [prat_less_trans],
diff -r 1a85ba81d019 -r 1be9b63e7d93 src/HOL/Real/PReal.ML
--- a/src/HOL/Real/PReal.ML	Mon Oct 11 10:51:24 1999 +0200
+++ b/src/HOL/Real/PReal.ML	Mon Oct 11 10:52:51 1999 +0200
@@ -51,21 +51,21 @@
 qed "mem_Rep_preal_Ex";
 
 Goalw [preal_def] 
-      "[| {} < A; A < {q::prat. True}; \
+      "[| {} < A; A < UNIV; \
 \              (!y: A. ((!z. z < y --> z: A) & \
 \                        (? u: A. y < u))) |] ==> A : preal";
 by (Fast_tac 1);
 qed "prealI1";
     
 Goalw [preal_def] 
-      "[| {} < A; A < {q::prat. True}; \
+      "[| {} < A; A < UNIV; \
 \              !y: A. (!z. z < y --> z: A); \
 \              !y: A. (? u: A. y < u) |] ==> A : preal";
 by (Best_tac 1);
 qed "prealI2";
 
 Goalw [preal_def] 
-      "A : preal ==> {} < A & A < {q::prat. True} & \
+      "A : preal ==> {} < A & A < UNIV & \
 \                         (!y: A. ((!z. z < y --> z: A) & \
 \                                  (? u: A. y < u)))";
 by (Fast_tac 1);
@@ -81,7 +81,7 @@
 by (Fast_tac 1);
 qed "prealE_lemma1";
 
-Goalw [preal_def] "A : preal ==> A < {q::prat. True}";
+Goalw [preal_def] "A : preal ==> A < UNIV";
 by (Fast_tac 1);
 qed "prealE_lemma2";
 
@@ -235,7 +235,7 @@
 by (auto_tac (claset(),simpset() addsimps [prat_less_not_refl]));
 qed "preal_not_mem_add_set_Ex";
 
-Goal "{w. ? x: Rep_preal R. ? y:Rep_preal S. w = x + y} < {q. True}";
+Goal "{w. ? x: Rep_preal R. ? y:Rep_preal S. w = x + y} < UNIV";
 by (auto_tac (claset() addSIs [psubsetI],simpset()));
 by (cut_inst_tac [("R","R"),("S","S")] preal_not_mem_add_set_Ex 1);
 by (etac exE 1);
@@ -325,7 +325,7 @@
 by (auto_tac (claset(),simpset() addsimps [prat_less_not_refl]));
 qed "preal_not_mem_mult_set_Ex";
 
-Goal "{w. ? x: Rep_preal R. ? y:Rep_preal S. w = x * y} < {q. True}";
+Goal "{w. ? x: Rep_preal R. ? y:Rep_preal S. w = x * y} < UNIV";
 by (auto_tac (claset() addSIs [psubsetI],simpset()));
 by (cut_inst_tac [("R","R"),("S","S")] preal_not_mem_mult_set_Ex 1);
 by (etac exE 1);
@@ -555,7 +555,7 @@
 by (auto_tac (claset(),simpset() addsimps [prat_less_not_refl]));
 qed "preal_not_mem_inv_set_Ex";
 
-Goal "{x. ? y. x < y & qinv y ~:  Rep_preal A} < {q. True}";
+Goal "{x. ? y. x < y & qinv y ~:  Rep_preal A} < UNIV";
 by (auto_tac (claset() addSIs [psubsetI],simpset()));
 by (cut_inst_tac [("A","A")]  preal_not_mem_inv_set_Ex 1);
 by (etac exE 1);
@@ -877,7 +877,7 @@
 by (auto_tac (claset() addDs [Rep_preal RS prealE_lemma3b],simpset()));
 qed "lemma_ex_not_mem_less_left_add1";
 
-Goal "{d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)} < {q. True}";
+Goal "{d. ? n. n ~: Rep_preal(A) & n + d : Rep_preal(B)} < UNIV";
 by (auto_tac (claset() addSIs [psubsetI],simpset()));
 by (cut_inst_tac [("A","A"),("B","B")] lemma_ex_not_mem_less_left_add1 1);
 by (etac exE 1);
@@ -1115,7 +1115,7 @@
 qed "preal_sup_not_mem_Ex1";
 
 Goal "? Y. (! X: P. X < Y)  \                                    
-\         ==> {w. ? X: P. w: Rep_preal(X)} < {q. True}";       (**)
+\         ==> {w. ? X: P. w: Rep_preal(X)} < UNIV";       (**)
 by (dtac preal_sup_not_mem_Ex 1);
 by (auto_tac (claset() addSIs [psubsetI],simpset()));
 by (eres_inst_tac [("c","q")] equalityCE 1);
@@ -1123,7 +1123,7 @@
 qed "preal_sup_set_not_prat_set";
 
 Goal "? Y. (! X: P. X <= Y)  \
-\         ==> {w. ? X: P. w: Rep_preal(X)} < {q. True}";
+\         ==> {w. ? X: P. w: Rep_preal(X)} < UNIV";
 by (dtac preal_sup_not_mem_Ex1 1);
 by (auto_tac (claset() addSIs [psubsetI],simpset()));
 by (eres_inst_tac [("c","q")] equalityCE 1);
diff -r 1a85ba81d019 -r 1be9b63e7d93 src/HOL/Real/PReal.thy
--- a/src/HOL/Real/PReal.thy	Mon Oct 11 10:51:24 1999 +0200
+++ b/src/HOL/Real/PReal.thy	Mon Oct 11 10:52:51 1999 +0200
@@ -9,7 +9,7 @@
 
 PReal = PRat +
 
-typedef preal = "{A::prat set. {} < A & A < {q::prat. True} &
+typedef preal = "{A::prat set. {} < A & A < UNIV &
                                (!y: A. ((!z. z < y --> z: A) &
                                         (? u: A. y < u)))}"      (preal_1)
 instance