src/HOL/Set.thy
changeset 17084 fb0a80aef0be
parent 17002 fb9261990ffe
child 17085 5b57f995a179
     1.1 --- a/src/HOL/Set.thy	Tue Aug 16 13:54:24 2005 +0200
     1.2 +++ b/src/HOL/Set.thy	Tue Aug 16 15:36:28 2005 +0200
     1.3 @@ -671,10 +671,10 @@
     1.4    Classical prover.  Negated assumptions behave like formulae on the
     1.5    right side of the notional turnstile ... *}
     1.6  
     1.7 -lemma ComplD: "c : -A ==> c~:A"
     1.8 +lemma ComplD [dest!]: "c : -A ==> c~:A"
     1.9    by (unfold Compl_def) blast
    1.10  
    1.11 -lemmas ComplE [elim!] = ComplD [elim_format]
    1.12 +lemmas ComplE = ComplD [elim_format]
    1.13  
    1.14  
    1.15  subsubsection {* Binary union -- Un *}
    1.16 @@ -764,10 +764,10 @@
    1.17      -- {* Redundant? But unlike @{text insertCI}, it proves the subgoal immediately! *}
    1.18    by (rule insertI1)
    1.19  
    1.20 -lemma singletonD: "b : {a} ==> b = a"
    1.21 +lemma singletonD [dest!]: "b : {a} ==> b = a"
    1.22    by blast
    1.23  
    1.24 -lemmas singletonE [elim!] = singletonD [elim_format]
    1.25 +lemmas singletonE = singletonD [elim_format]
    1.26  
    1.27  lemma singleton_iff: "(b : {a}) = (b = a)"
    1.28    by blast