equal
deleted
inserted
replaced
100 lemma givenBy_DiffI: |
100 lemma givenBy_DiffI: |
101 "[| A : givenBy v; B : givenBy v |] ==> A-B : givenBy v" |
101 "[| A : givenBy v; B : givenBy v |] ==> A-B : givenBy v" |
102 apply (simp (no_asm_use) add: givenBy_eq_Collect) |
102 apply (simp (no_asm_use) add: givenBy_eq_Collect) |
103 apply safe |
103 apply safe |
104 apply (rule_tac x = "%z. ?R z & ~ ?Q z" in exI) |
104 apply (rule_tac x = "%z. ?R z & ~ ?Q z" in exI) |
105 unfolding set_diff_def |
105 unfolding set_diff_eq |
106 apply auto |
106 apply auto |
107 done |
107 done |
108 |
108 |
109 |
109 |
110 (** Standard leadsTo rules **) |
110 (** Standard leadsTo rules **) |