--- 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 <> ***)
(* ------------------------------------------------------------------------- *)