--- a/doc-src/Logics/CTT-eg.txt Fri Nov 12 10:41:13 1993 +0100
+++ b/doc-src/Logics/CTT-eg.txt Fri Nov 12 11:43:35 1993 +0100
@@ -6,7 +6,7 @@
(*** Type inference, from CTT/ex/typechk.ML ***)
-goal CTT_Rule.thy "lam n. rec(n, 0, %x y.x) : ?A";
+goal CTT.thy "lam n. rec(n, 0, %x y.x) : ?A";
by (resolve_tac [ProdI] 1);
by (eresolve_tac [NE] 2);
by (resolve_tac [NI0] 2);
@@ -17,7 +17,7 @@
(*** Logical reasoning, from CTT/ex/elim.ML ***)
-val prems = goal CTT_Rule.thy
+val prems = goal CTT.thy
"[| A type; \
\ !!x. x:A ==> B(x) type; \
\ !!x. x:A ==> C(x) type; \
@@ -35,7 +35,7 @@
(*** Currying, from CTT/ex/elim.ML ***)
-val prems = goal CTT_Rule.thy
+val prems = goal CTT.thy
"[| A type; !!x. x:A ==> B(x) type; \
\ !!z. z: (SUM x:A. B(x)) ==> C(z) type |] \
\ ==> ?a : (PROD z : (SUM x:A . B(x)) . C(z)) \
@@ -47,7 +47,7 @@
(*** Axiom of Choice ***)
-val prems = goal CTT_Rule.thy
+val prems = goal CTT.thy
"[| A type; !!x. x:A ==> B(x) type; \
\ !!x y.[| x:A; y:B(x) |] ==> C(x,y) type \
\ |] ==> ?a : (PROD x:A. SUM y:B(x). C(x,y)) \
@@ -65,7 +65,7 @@
-> goal CTT_Rule.thy "lam n. rec(n, 0, %x y.x) : ?A";
+> goal CTT.thy "lam n. rec(n, 0, %x y.x) : ?A";
Level 0
lam n. rec(n,0,%x y. x) : ?A
1. lam n. rec(n,0,%x y. x) : ?A
@@ -97,7 +97,7 @@
-> val prems = goal CTT_Rule.thy
+> val prems = goal CTT.thy
# "[| A type; \
# \ !!x. x:A ==> B(x) type; \
# \ !!x. x:A ==> C(x) type; \
@@ -174,7 +174,7 @@
-> val prems = goal CTT_Rule.thy
+> val prems = goal CTT.thy
# "[| A type; !!x. x:A ==> B(x) type; \
# \ !!z. z: (SUM x:A. B(x)) ==> C(z) type |] \
# \ ==> ?a : (PROD z : (SUM x:A . B(x)) . C(z)) \
@@ -204,7 +204,7 @@
-> val prems = goal CTT_Rule.thy
+> val prems = goal CTT.thy
# "[| A type; !!x. x:A ==> B(x) type; \
# \ !!x y.[| x:A; y:B(x) |] ==> C(x,y) type \
# \ |] ==> ?a : (PROD x:A. SUM y:B(x). C(x,y)) \
--- a/doc-src/Logics/ZF-eg.txt Fri Nov 12 10:41:13 1993 +0100
+++ b/doc-src/Logics/ZF-eg.txt Fri Nov 12 11:43:35 1993 +0100
@@ -5,7 +5,7 @@
(*** Powerset example ***)
-val [prem] = goal ZF_Rule.thy "A<=B ==> Pow(A) <= Pow(B)";
+val [prem] = goal ZF.thy "A<=B ==> Pow(A) <= Pow(B)";
by (resolve_tac [subsetI] 1);
by (resolve_tac [PowI] 1);
by (dresolve_tac [PowD] 1);
@@ -13,7 +13,7 @@
by (resolve_tac [prem] 1);
val Pow_mono = result();
-goal ZF_Rule.thy "Pow(A Int B) = Pow(A) Int Pow(B)";
+goal ZF.thy "Pow(A Int B) = Pow(A) Int Pow(B)";
by (resolve_tac [equalityI] 1);
by (resolve_tac [Int_greatest] 1);
by (resolve_tac [Int_lower1 RS Pow_mono] 1);
@@ -27,7 +27,7 @@
choplev 0;
by (fast_tac (ZF_cs addIs [equalityI]) 1);
-val [prem] = goal ZF_Rule.thy "C<=D ==> Union(C) <= Union(D)";
+val [prem] = goal ZF.thy "C<=D ==> Union(C) <= Union(D)";
by (resolve_tac [subsetI] 1);
by (eresolve_tac [UnionE] 1);
by (resolve_tac [UnionI] 1);
@@ -40,7 +40,7 @@
by (eresolve_tac [prem RS subsetD] 1);
-val prems = goal ZF_Rule.thy
+val prems = goal ZF.thy
"[| a:A; f: A->B; g: C->D; A Int C = 0 |] ==> \
\ (f Un g)`a = f`a";
by (resolve_tac [apply_equality] 1);
@@ -56,13 +56,13 @@
-goal ZF_Rule.thy "f``(UN x:A. B(x)) = (UN x:A. f``B(x))";
+goal ZF.thy "f``(UN x:A. B(x)) = (UN x:A. f``B(x))";
by (resolve_tac [equalityI] 1);
by (resolve_tac [subsetI] 1);
fe imageE;
-goal ZF_Rule.thy "(UN x:C. A(x) Int B) = (UN x:C. A(x)) Int B";
+goal ZF.thy "(UN x:C. A(x) Int B) = (UN x:C. A(x)) Int B";
by (resolve_tac [equalityI] 1);
by (resolve_tac [Int_greatest] 1);
fr UN_mono;
@@ -71,7 +71,7 @@
????
-> goal ZF_Rule.thy "Pow(A Int B) = Pow(A) Int Pow(B)";
+> goal ZF.thy "Pow(A Int B) = Pow(A) Int Pow(B)";
Level 0
Pow(A Int B) = Pow(A) Int Pow(B)
1. Pow(A Int B) = Pow(A) Int Pow(B)
@@ -132,7 +132,7 @@
-> val [prem] = goal ZF_Rule.thy "C<=D ==> Union(C) <= Union(D)";
+> val [prem] = goal ZF.thy "C<=D ==> Union(C) <= Union(D)";
Level 0
Union(C) <= Union(D)
1. Union(C) <= Union(D)
@@ -165,7 +165,7 @@
-> val prems = goal ZF_Rule.thy
+> val prems = goal ZF.thy
# "[| a:A; f: A->B; g: C->D; A Int C = 0 |] ==> \
# \ (f Un g)`a = f`a";
Level 0