equal
deleted
inserted
replaced
130 (*Fake*) |
130 (*Fake*) |
131 by (best_tac |
131 by (best_tac |
132 (!claset addIs [impOfSubs analz_subset_parts] |
132 (!claset addIs [impOfSubs analz_subset_parts] |
133 addDs [impOfSubs (analz_subset_parts RS keysFor_mono), |
133 addDs [impOfSubs (analz_subset_parts RS keysFor_mono), |
134 impOfSubs (parts_insert_subset_Un RS keysFor_mono)] |
134 impOfSubs (parts_insert_subset_Un RS keysFor_mono)] |
135 unsafe_addss (!simpset)) 1); |
135 addss (!simpset)) 1); |
136 by (ALLGOALS Blast_tac); |
136 by (ALLGOALS Blast_tac); |
137 qed_spec_mp "new_keys_not_used"; |
137 qed_spec_mp "new_keys_not_used"; |
138 |
138 |
139 bind_thm ("new_keys_not_analzd", |
139 bind_thm ("new_keys_not_analzd", |
140 [analz_subset_parts RS keysFor_mono, |
140 [analz_subset_parts RS keysFor_mono, |