src/FOL/IFOL.thy
changeset 39159 0dec18004e75
parent 38522 de7984a7172b
child 39557 fe5722fce758
     1.1 --- a/src/FOL/IFOL.thy	Mon Sep 06 19:11:01 2010 +0200
     1.2 +++ b/src/FOL/IFOL.thy	Mon Sep 06 19:13:10 2010 +0200
     1.3 @@ -340,7 +340,7 @@
     1.4    shows "(P&Q) <-> (P'&Q')"
     1.5    apply (insert assms)
     1.6    apply (assumption | rule iffI conjI | erule iffE conjE mp |
     1.7 -    tactic {* iff_tac (thms "assms") 1 *})+
     1.8 +    tactic {* iff_tac @{thms assms} 1 *})+
     1.9    done
    1.10  
    1.11  (*Reversed congruence rule!   Used in ZF/Order*)
    1.12 @@ -350,7 +350,7 @@
    1.13    shows "(Q&P) <-> (Q'&P')"
    1.14    apply (insert assms)
    1.15    apply (assumption | rule iffI conjI | erule iffE conjE mp |
    1.16 -    tactic {* iff_tac (thms "assms") 1 *})+
    1.17 +    tactic {* iff_tac @{thms assms} 1 *})+
    1.18    done
    1.19  
    1.20  lemma disj_cong:
    1.21 @@ -366,7 +366,7 @@
    1.22    shows "(P-->Q) <-> (P'-->Q')"
    1.23    apply (insert assms)
    1.24    apply (assumption | rule iffI impI | erule iffE | erule (1) notE impE |
    1.25 -    tactic {* iff_tac (thms "assms") 1 *})+
    1.26 +    tactic {* iff_tac @{thms assms} 1 *})+
    1.27    done
    1.28  
    1.29  lemma iff_cong: "[| P <-> P'; Q <-> Q' |] ==> (P<->Q) <-> (P'<->Q')"
    1.30 @@ -381,21 +381,21 @@
    1.31    assumes "!!x. P(x) <-> Q(x)"
    1.32    shows "(ALL x. P(x)) <-> (ALL x. Q(x))"
    1.33    apply (assumption | rule iffI allI | erule (1) notE impE | erule allE |
    1.34 -    tactic {* iff_tac (thms "assms") 1 *})+
    1.35 +    tactic {* iff_tac @{thms assms} 1 *})+
    1.36    done
    1.37  
    1.38  lemma ex_cong:
    1.39    assumes "!!x. P(x) <-> Q(x)"
    1.40    shows "(EX x. P(x)) <-> (EX x. Q(x))"
    1.41    apply (erule exE | assumption | rule iffI exI | erule (1) notE impE |
    1.42 -    tactic {* iff_tac (thms "assms") 1 *})+
    1.43 +    tactic {* iff_tac @{thms assms} 1 *})+
    1.44    done
    1.45  
    1.46  lemma ex1_cong:
    1.47    assumes "!!x. P(x) <-> Q(x)"
    1.48    shows "(EX! x. P(x)) <-> (EX! x. Q(x))"
    1.49    apply (erule ex1E spec [THEN mp] | assumption | rule iffI ex1I | erule (1) notE impE |
    1.50 -    tactic {* iff_tac (thms "assms") 1 *})+
    1.51 +    tactic {* iff_tac @{thms assms} 1 *})+
    1.52    done
    1.53  
    1.54  (*** Equality rules ***)