src/Cube/Cube.ML

--- a/src/Cube/Cube.ML	Thu Jun 09 11:09:45 1994 +0200
+++ b/src/Cube/Cube.ML	Thu Jun 09 11:11:03 1994 +0200
@@ -1,35 +1,35 @@
-(*  Title: 	Cube/cube
+(*  Title:      Cube/Cube.ML
     ID:         $Id$
-    Author: 	Tobias Nipkow
+    Author:     Tobias Nipkow
     Copyright   1990  University of Cambridge
 
-For cube.thy.  The systems of the Lambda-cube that extend simple types
+For Cube.thy.  The systems of the Lambda-cube that extend simple types
 *)
 
 open Cube;
 
 val simple = [s_b,strip_s,strip_b,app,lam_ss,pi_ss];
 
-val L2_thy = extend_theory Cube.thy "L2" ([],[],[],[],[],[],None)
-[
-  ("pi_bs",  "[| A:[]; !!x. x:A ==> B(x):* |] ==> Prod(A,B):*"),
-
-  ("lam_bs", "[| A:[]; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* |] \
-\	==> Abs(A,f) : Prod(A,B)")
-];
+val L2_thy =
+  Cube.thy
+  |> add_axioms
+   [("pi_bs",  "[| A:[]; !!x. x:A ==> B(x):* |] ==> Prod(A,B):*"),
+    ("lam_bs", "[| A:[]; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):* |] \
+     \  ==> Abs(A,f) : Prod(A,B)")]
+  |> add_thyname "L2";
 
 val lam_bs = get_axiom L2_thy "lam_bs";
 val pi_bs = get_axiom L2_thy "pi_bs";
 
 val L2 = simple @ [lam_bs,pi_bs];
 
-val Lomega_thy = extend_theory Cube.thy "Lomega" ([],[],[],[],[],[],None)
-[
-  ("pi_bb",  "[| A:[]; !!x. x:A ==> B(x):[] |] ==> Prod(A,B):[]"),
-
-  ("lam_bb", "[| A:[]; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):[] |] \
-\	==> Abs(A,f) : Prod(A,B)")
-];
+val Lomega_thy =
+  Cube.thy
+  |> add_axioms
+   [("pi_bb",  "[| A:[]; !!x. x:A ==> B(x):[] |] ==> Prod(A,B):[]"),
+    ("lam_bb", "[| A:[]; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):[] |] \
+     \  ==> Abs(A,f) : Prod(A,B)")]
+  |> add_thyname "Lomega";
 
 val lam_bb = get_axiom Lomega_thy "lam_bb";
 val pi_bb = get_axiom Lomega_thy "pi_bb";
@@ -38,13 +38,13 @@
 val LOmega_thy = merge_theories(L2_thy,Lomega_thy);
 val LOmega = simple @ [lam_bs,pi_bs,lam_bb,pi_bb];
 
-val LP_thy = extend_theory Cube.thy "LP" ([],[],[],[],[],[],None)
-[
-  ("pi_sb",  "[| A:*; !!x. x:A ==> B(x):[] |] ==> Prod(A,B):[]"),
-
-  ("lam_sb", "[| A:*; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):[] |] \
-\	==> Abs(A,f) : Prod(A,B)")
-];
+val LP_thy =
+  Cube.thy
+  |> add_axioms
+   [("pi_sb",  "[| A:*; !!x. x:A ==> B(x):[] |] ==> Prod(A,B):[]"),
+    ("lam_sb", "[| A:*; !!x. x:A ==> f(x):B(x); !!x. x:A ==> B(x):[] |] \
+     \  ==> Abs(A,f) : Prod(A,B)")]
+  |> add_thyname "LP";
 
 val lam_sb = get_axiom LP_thy "lam_sb";
 val pi_sb = get_axiom LP_thy "pi_sb";