tuned;
authorwenzelm
Wed Apr 10 11:51:56 2013 +0200 (2013-04-10)
changeset 516685e1108291c7f
parent 51667 354c23ef2784
child 51669 7fbc4fc400d8
tuned;
src/HOL/TLA/TLA.thy
     1.1 --- a/src/HOL/TLA/TLA.thy	Tue Apr 09 21:39:55 2013 +0200
     1.2 +++ b/src/HOL/TLA/TLA.thy	Wed Apr 10 11:51:56 2013 +0200
     1.3 @@ -102,12 +102,12 @@
     1.4  
     1.5  (* Specialize intensional introduction/elimination rules for temporal formulas *)
     1.6  
     1.7 -lemma tempI: "(!!sigma. sigma |= (F::temporal)) ==> |- F"
     1.8 +lemma tempI [intro!]: "(!!sigma. sigma |= (F::temporal)) ==> |- F"
     1.9    apply (rule intI)
    1.10    apply (erule meta_spec)
    1.11    done
    1.12  
    1.13 -lemma tempD: "|- (F::temporal) ==> sigma |= F"
    1.14 +lemma tempD [dest]: "|- (F::temporal) ==> sigma |= F"
    1.15    by (erule intD)
    1.16  
    1.17  
    1.18 @@ -139,15 +139,6 @@
    1.19  attribute_setup try_rewrite = {* Scan.succeed (Thm.rule_attribute (K try_rewrite)) *}
    1.20  
    1.21  
    1.22 -(* Update classical reasoner---will be updated once more below! *)
    1.23 -
    1.24 -declare tempI [intro!]
    1.25 -declare tempD [dest]
    1.26 -
    1.27 -(* Modify the functions that add rules to simpsets, classical sets,
    1.28 -   and clasimpsets in order to accept "lifted" theorems
    1.29 -*)
    1.30 -
    1.31  (* ------------------------------------------------------------------------- *)
    1.32  (***           "Simple temporal logic": only [] and <>                     ***)
    1.33  (* ------------------------------------------------------------------------- *)