# HG changeset patch
# User wenzelm
# Date 1365587516 -7200
# Node ID 5e1108291c7fabe1b342416e893f8000414158d8
# Parent  354c23ef2784371a390a627ab9a425f9f5d6b546
tuned;

diff -r 354c23ef2784 -r 5e1108291c7f src/HOL/TLA/TLA.thy
--- a/src/HOL/TLA/TLA.thy	Tue Apr 09 21:39:55 2013 +0200
+++ b/src/HOL/TLA/TLA.thy	Wed Apr 10 11:51:56 2013 +0200
@@ -102,12 +102,12 @@
 
 (* Specialize intensional introduction/elimination rules for temporal formulas *)
 
-lemma tempI: "(!!sigma. sigma |= (F::temporal)) ==> |- F"
+lemma tempI [intro!]: "(!!sigma. sigma |= (F::temporal)) ==> |- F"
   apply (rule intI)
   apply (erule meta_spec)
   done
 
-lemma tempD: "|- (F::temporal) ==> sigma |= F"
+lemma tempD [dest]: "|- (F::temporal) ==> sigma |= F"
   by (erule intD)
 
 
@@ -139,15 +139,6 @@
 attribute_setup try_rewrite = {* Scan.succeed (Thm.rule_attribute (K try_rewrite)) *}
 
 
-(* Update classical reasoner---will be updated once more below! *)
-
-declare tempI [intro!]
-declare tempD [dest]
-
-(* Modify the functions that add rules to simpsets, classical sets,
-   and clasimpsets in order to accept "lifted" theorems
-*)
-
 (* ------------------------------------------------------------------------- *)
 (***           "Simple temporal logic": only [] and <>                     ***)
 (* ------------------------------------------------------------------------- *)