--- 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";