Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Cube/Cube.ML
changeset 4026 b94dc94be4b7
parent 3884 5423e06b9fe6 
--- 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)")]
isabelle