Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
added empty type-abbr field to extend_theory
authornipkow
Tue, 21 Dec 1993 16:40:01 +0100
changeset 203 4a213aaca3d9
parent 202 4e68398cdc06
child 204 b9f087b42a44
added empty type-abbr field to extend_theory
src/Cube/Cube.ML file | annotate | diff | comparison | revisions
src/Cube/cube.ML file | annotate | diff | comparison | revisions
src/LCF/ex.ML file | annotate | diff | comparison | revisions 
--- a/src/Cube/Cube.ML	Tue Dec 21 16:38:45 1993 +0100
+++ b/src/Cube/Cube.ML	Tue Dec 21 16:40:01 1993 +0100
@@ -10,7 +10,7 @@
 
 val simple = [s_b,strip_s,strip_b,app,lam_ss,pi_ss];
 
-val L2_thy = extend_theory Cube.thy "L2" ([],[],[],[],[],None)
+val L2_thy = extend_theory Cube.thy "L2" ([],[],[],[],[],[],None)
 [
   ("pi_bs",  "[| A:[]; !!x. x:A ==> B(x):* |] ==> Prod(A,B):*"),
 
@@ -23,7 +23,7 @@
 
 val L2 = simple @ [lam_bs,pi_bs];
 
-val Lomega_thy = extend_theory Cube.thy "Lomega" ([],[],[],[],[],None)
+val Lomega_thy = extend_theory Cube.thy "Lomega" ([],[],[],[],[],[],None)
 [
   ("pi_bb",  "[| A:[]; !!x. x:A ==> B(x):[] |] ==> Prod(A,B):[]"),
 
@@ -38,7 +38,7 @@
 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)
+val LP_thy = extend_theory Cube.thy "LP" ([],[],[],[],[],[],None)
 [
   ("pi_sb",  "[| A:*; !!x. x:A ==> B(x):[] |] ==> Prod(A,B):[]"),
 
--- a/src/Cube/cube.ML	Tue Dec 21 16:38:45 1993 +0100
+++ b/src/Cube/cube.ML	Tue Dec 21 16:40:01 1993 +0100
@@ -10,7 +10,7 @@
 
 val simple = [s_b,strip_s,strip_b,app,lam_ss,pi_ss];
 
-val L2_thy = extend_theory Cube.thy "L2" ([],[],[],[],[],None)
+val L2_thy = extend_theory Cube.thy "L2" ([],[],[],[],[],[],None)
 [
   ("pi_bs",  "[| A:[]; !!x. x:A ==> B(x):* |] ==> Prod(A,B):*"),
 
@@ -23,7 +23,7 @@
 
 val L2 = simple @ [lam_bs,pi_bs];
 
-val Lomega_thy = extend_theory Cube.thy "Lomega" ([],[],[],[],[],None)
+val Lomega_thy = extend_theory Cube.thy "Lomega" ([],[],[],[],[],[],None)
 [
   ("pi_bb",  "[| A:[]; !!x. x:A ==> B(x):[] |] ==> Prod(A,B):[]"),
 
@@ -38,7 +38,7 @@
 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)
+val LP_thy = extend_theory Cube.thy "LP" ([],[],[],[],[],[],None)
 [
   ("pi_sb",  "[| A:*; !!x. x:A ==> B(x):[] |] ==> Prod(A,B):[]"),
 
--- a/src/LCF/ex.ML	Tue Dec 21 16:38:45 1993 +0100
+++ b/src/LCF/ex.ML	Tue Dec 21 16:40:01 1993 +0100
@@ -14,7 +14,7 @@
 (***  Section 10.4  ***)
 
 val ex_thy = extend_theory thy "Ex 10.4"
-([], [], [], [],
+([], [], [], [], [],
  [(["P"], "'a => tr"),
   (["G","H"], "'a => 'a"),
   (["K"], "('a => 'a) => ('a => 'a)")
@@ -56,7 +56,7 @@
 (***  Example 3.8  ***)
 
 val ex_thy = extend_theory thy "Ex 3.8"
-([], [], [], [],
+([], [], [], [], [],
  [(["P"], "'a => tr"),
   (["F","G"], "'a => 'a"),
   (["H"], "'a => 'b => 'b"),
@@ -86,7 +86,7 @@
 (*** Addition with fixpoint of successor ***)
 
 val ex_thy = extend_theory thy "fix ex"
-([], [], [], [],
+([], [], [], [], [],
  [(["s"], "'a => 'a"),
   (["p"], "'a => 'a => 'a")
  ],
isabelle