--- 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";
--- a/src/LCF/ex.ML Thu Jun 09 11:09:45 1994 +0200
+++ b/src/LCF/ex.ML Thu Jun 09 11:11:03 1994 +0200
@@ -1,29 +1,31 @@
-(* Title: LCF/ex.ML
+(* Title: LCF/ex.ML
ID: $Id$
- Author: Tobias Nipkow
+ Author: Tobias Nipkow
Copyright 1991 University of Cambridge
Some examples from Lawrence Paulson's book Logic and Computation.
*)
-LCF_build_completed; (*Cause examples to fail if LCF did*)
+LCF_build_completed; (*Cause examples to fail if LCF did*)
proof_timing := true;
(*** Section 10.4 ***)
-val ex_thy = extend_theory thy "Ex 10.4"
-([], [], [], [], [],
- [(["P"], "'a => tr"),
- (["G","H"], "'a => 'a"),
- (["K"], "('a => 'a) => ('a => 'a)")
- ],
- None)
-[ ("P_strict", "P(UU) = UU"),
- ("K", "K = (%h x. P(x) => x | h(h(G(x))))"),
- ("H", "H = FIX(K)")
-];
+val ex_thy =
+ thy
+ |> add_consts
+ [("P", "'a => tr", NoSyn),
+ ("G", "'a => 'a", NoSyn),
+ ("H", "'a => 'a", NoSyn),
+ ("K", "('a => 'a) => ('a => 'a)", NoSyn)]
+ |> add_axioms
+ [("P_strict", "P(UU) = UU"),
+ ("K", "K = (%h x. P(x) => x | h(h(G(x))))"),
+ ("H", "H = FIX(K)")]
+ |> add_thyname "Ex 10.4";
+
val ax = get_axiom ex_thy;
val P_strict = ax"P_strict";
@@ -55,18 +57,20 @@
(*** Example 3.8 ***)
-val ex_thy = extend_theory thy "Ex 3.8"
-([], [], [], [], [],
- [(["P"], "'a => tr"),
- (["F","G"], "'a => 'a"),
- (["H"], "'a => 'b => 'b"),
- (["K"], "('a => 'b => 'b) => ('a => 'b => 'b)")
- ],
- None)
-[ ("F_strict", "F(UU) = UU"),
- ("K", "K = (%h x y. P(x) => y | F(h(G(x),y)))"),
- ("H", "H = FIX(K)")
-];
+val ex_thy =
+ thy
+ |> add_consts
+ [("P", "'a => tr", NoSyn),
+ ("F", "'a => 'a", NoSyn),
+ ("G", "'a => 'a", NoSyn),
+ ("H", "'a => 'b => 'b", NoSyn),
+ ("K", "('a => 'b => 'b) => ('a => 'b => 'b)", NoSyn)]
+ |> add_axioms
+ [("F_strict", "F(UU) = UU"),
+ ("K", "K = (%h x y. P(x) => y | F(h(G(x),y)))"),
+ ("H", "H = FIX(K)")]
+ |> add_thyname "Ex 3.8";
+
val ax = get_axiom ex_thy;
val F_strict = ax"F_strict";
@@ -85,15 +89,16 @@
(*** Addition with fixpoint of successor ***)
-val ex_thy = extend_theory thy "fix ex"
-([], [], [], [], [],
- [(["s"], "'a => 'a"),
- (["p"], "'a => 'a => 'a")
- ],
- None)
-[ ("p_strict", "p(UU) = UU"),
- ("p_s", "p(s(x),y) = s(p(x,y))")
-];
+val ex_thy =
+ thy
+ |> add_consts
+ [("s", "'a => 'a", NoSyn),
+ ("p", "'a => 'a => 'a", NoSyn)]
+ |> add_axioms
+ [("p_strict", "p(UU) = UU"),
+ ("p_s", "p(s(x),y) = s(p(x,y))")]
+ |> add_thyname "fix ex";
+
val ax = get_axiom ex_thy;
val p_strict = ax"p_strict";