--- a/src/Cube/Cube.ML Tue Oct 28 17:41:40 1997 +0100
+++ b/src/Cube/Cube.ML Tue Oct 28 17:56:15 1997 +0100
@@ -12,7 +12,7 @@
val L2_thy =
Cube.thy
- |> Theory.add_axioms
+ |> PureThy.add_store_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)")]
@@ -25,7 +25,7 @@
val Lomega_thy =
Cube.thy
- |> Theory.add_axioms
+ |> PureThy.add_store_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)")]
@@ -40,7 +40,7 @@
val LP_thy =
Cube.thy
- |> Theory.add_axioms
+ |> PureThy.add_store_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)")]