# HG changeset patch
# User lcp
# Date 753101015 -3600
# Node ID 745affa0262b34651bbded40d9778434a2c46a3e
# Parent  96c627d2815ea78c41f2b91f9b0f7d3d97b63512
Misc updates

diff -r 96c627d2815e -r 745affa0262b doc-src/Logics/CTT-eg.txt
--- 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))    \
diff -r 96c627d2815e -r 745affa0262b doc-src/Logics/ZF-eg.txt
--- 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