# HG changeset patch
# User paulson
# Date 911208990 -3600
# Node ID 2303f5a3036d9d92ff81090b2fc94071e732e0b7
# Parent  30b6a32518130fc30d6a52284c7235e73bf8c10e
moved some facts about Pi from ex/PiSets to Fun.ML

diff -r 30b6a3251813 -r 2303f5a3036d src/HOL/Fun.ML
--- a/src/HOL/Fun.ML	Sat Nov 14 13:26:11 1998 +0100
+++ b/src/HOL/Fun.ML	Mon Nov 16 10:36:30 1998 +0100
@@ -375,4 +375,11 @@
 by (auto_tac (claset(), simpset() addsimps [split_if_mem1, split_if_eq1]));
 qed "Applyall_beta";
 
+Goal "Pi {} B = { (%x. @ y. True) }";
+by (auto_tac (claset() addIs [ext], simpset() addsimps [Pi_def]));
+qed "Pi_empty";
 
+val [major] = Goalw [Pi_def] "(!!x. x: A ==> B x <= C x) ==> Pi A B <= Pi A C";
+by (auto_tac (claset(),
+	      simpset() addsimps [impOfSubs major]));
+qed "Pi_mono";
diff -r 30b6a3251813 -r 2303f5a3036d src/HOL/ex/PiSets.ML
--- a/src/HOL/ex/PiSets.ML	Sat Nov 14 13:26:11 1998 +0100
+++ b/src/HOL/ex/PiSets.ML	Mon Nov 16 10:36:30 1998 +0100
@@ -85,15 +85,3 @@
 by (assume_tac 1);
 qed "PiBij_bij2";
 
-Goal "Pi {} B = {f. !x. f x = (@ y. True)}";
-by (asm_full_simp_tac (simpset() addsimps [Pi_def]) 1);
-qed "empty_Pi";
-
-Goal "(% x. (@ y. True)) : Pi {} B";
-by (simp_tac (simpset() addsimps [empty_Pi]) 1);
-qed "empty_Pi_func";
-
-val [major] = Goalw [Pi_def] "(!!x. x: A ==> B x <= C x) ==> Pi A B <= Pi A C";
-by (auto_tac (claset(),
-	      simpset() addsimps [impOfSubs major]));
-qed "Pi_mono";