# HG changeset patch
# User wenzelm
# Date 1349874080 -7200
# Node ID 2bbb0013ff82182afe38b2e323cc0b18b0ff752a
# Parent  5248806bc7abee4a116b18935f3272502e0acd5d
modernized dynamic "rules" -- avoid rebinding of static facts;

diff -r 5248806bc7ab -r 2bbb0013ff82 src/Cube/Cube.thy
--- 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