--- a/src/Cube/Cube.thy Tue Oct 09 22:24:24 2012 +0200
+++ b/src/Cube/Cube.thy Wed Oct 10 15:01:20 2012 +0200
@@ -10,6 +10,15 @@
setup Pure_Thy.old_appl_syntax_setup
+ML {*
+ structure Rules = Named_Thms
+ (
+ val name = @{binding rules}
+ val description = "Cube inference rules"
+ )
+*}
+setup Rules.setup
+
typedecl "term"
typedecl "context"
typedecl typing
@@ -72,8 +81,7 @@
beta: "Abs(A, f)^a == f(a)"
-lemmas simple = s_b strip_s strip_b app lam_ss pi_ss
-lemmas rules = simple
+lemmas [rules] = s_b strip_s strip_b app lam_ss pi_ss
lemma imp_elim:
assumes "f:A\<rightarrow>B" and "a:A" and "f^a:B ==> PROP P"
@@ -90,7 +98,7 @@
==> Abs(A,f) : Prod(A,B)"
begin
-lemmas rules = simple lam_bs pi_bs
+lemmas [rules] = lam_bs pi_bs
end
@@ -102,7 +110,7 @@
==> Abs(A,f) : Prod(A,B)"
begin
-lemmas rules = simple lam_bb pi_bb
+lemmas [rules] = lam_bb pi_bb
end
@@ -113,7 +121,7 @@
==> Abs(A,f) : Prod(A,B)"
begin
-lemmas rules = simple lam_sb pi_sb
+lemmas [rules] = lam_sb pi_sb
end
@@ -121,7 +129,7 @@
locale LP2 = LP + L2
begin
-lemmas rules = simple lam_bs pi_bs lam_sb pi_sb
+lemmas [rules] = lam_bs pi_bs lam_sb pi_sb
end
@@ -129,7 +137,7 @@
locale Lomega2 = L2 + Lomega
begin
-lemmas rules = simple lam_bs pi_bs lam_bb pi_bb
+lemmas [rules] = lam_bs pi_bs lam_bb pi_bb
end
@@ -137,7 +145,7 @@
locale LPomega = LP + Lomega
begin
-lemmas rules = simple lam_bb pi_bb lam_sb pi_sb
+lemmas [rules] = lam_bb pi_bb lam_sb pi_sb
end
@@ -145,7 +153,7 @@
locale CC = L2 + LP + Lomega
begin
-lemmas rules = simple lam_bs pi_bs lam_bb pi_bb lam_sb pi_sb
+lemmas [rules] = lam_bs pi_bs lam_bb pi_bb lam_sb pi_sb
end