src/Sequents/ILL.thy
changeset 39159 0dec18004e75
parent 35113 1a0c129bb2e0
child 42814 5af15f1e2ef6
--- a/src/Sequents/ILL.thy	Mon Sep 06 19:11:01 2010 +0200
+++ b/src/Sequents/ILL.thy	Mon Sep 06 19:13:10 2010 +0200
@@ -126,24 +126,16 @@
 
 
 ML {*
-
 val lazy_cs = empty_pack
-  add_safes [thm "tensl", thm "conjr", thm "disjl", thm "promote0",
-    thm "context2", thm "context3"]
-  add_unsafes [thm "identity", thm "zerol", thm "conjll", thm "conjlr",
-    thm "disjrl", thm "disjrr", thm "impr", thm "tensr", thm "impl",
-    thm "derelict", thm "weaken", thm "promote1", thm "promote2",
-    thm "context1", thm "context4a", thm "context4b"];
+  add_safes [@{thm tensl}, @{thm conjr}, @{thm disjl}, @{thm promote0},
+    @{thm context2}, @{thm context3}]
+  add_unsafes [@{thm identity}, @{thm zerol}, @{thm conjll}, @{thm conjlr},
+    @{thm disjrl}, @{thm disjrr}, @{thm impr}, @{thm tensr}, @{thm impl},
+    @{thm derelict}, @{thm weaken}, @{thm promote1}, @{thm promote2},
+    @{thm context1}, @{thm context4a}, @{thm context4b}];
 
-local
-  val promote0 = thm "promote0"
-  val promote1 = thm "promote1"
-  val promote2 = thm "promote2"
-in
-
-fun prom_tac n = REPEAT (resolve_tac [promote0,promote1,promote2] n)
-
-end
+fun prom_tac n =
+  REPEAT (resolve_tac [@{thm promote0}, @{thm promote1}, @{thm promote2}] n)
 *}
 
 method_setup best_lazy =
@@ -272,13 +264,12 @@
   done
 
 ML {*
+val safe_cs = lazy_cs add_safes [@{thm conj_lemma}, @{thm ll_mp}, @{thm contrad1},
+                                 @{thm contrad2}, @{thm mp_rule1}, @{thm mp_rule2}, @{thm o_a_rule},
+                                 @{thm a_not_a_rule}]
+                      add_unsafes [@{thm aux_impl}];
 
-val safe_cs = lazy_cs add_safes [thm "conj_lemma", thm "ll_mp", thm "contrad1",
-                                 thm "contrad2", thm "mp_rule1", thm "mp_rule2", thm "o_a_rule",
-                                 thm "a_not_a_rule"]
-                      add_unsafes [thm "aux_impl"];
-
-val power_cs = safe_cs add_unsafes [thm "impr_contr_der"];
+val power_cs = safe_cs add_unsafes [@{thm impr_contr_der}];
 *}