equal
deleted
inserted
replaced
350 by (auto_tac (claset(), simpset() addsimps [ok_def])); |
350 by (auto_tac (claset(), simpset() addsimps [ok_def])); |
351 qed "ok_commute"; |
351 qed "ok_commute"; |
352 |
352 |
353 bind_thm ("ok_sym", ok_commute RS iffD1); |
353 bind_thm ("ok_sym", ok_commute RS iffD1); |
354 |
354 |
355 Goal "OK {(Numeral0::int,F),(Numeral1,G),(# 2,H)} snd = (F ok G & (F Join G) ok H)"; |
355 Goal "OK {(Numeral0::int,F),(Numeral1,G),(2,H)} snd = (F ok G & (F Join G) ok H)"; |
356 by (asm_full_simp_tac |
356 by (asm_full_simp_tac |
357 (simpset() addsimps [Ball_def, conj_disj_distribR, ok_def, Join_def, |
357 (simpset() addsimps [Ball_def, conj_disj_distribR, ok_def, Join_def, |
358 OK_def, insert_absorb, all_conj_distrib, eq_commute]) 1); |
358 OK_def, insert_absorb, all_conj_distrib, eq_commute]) 1); |
359 by (Blast_tac 1); |
359 by (Blast_tac 1); |
360 qed "ok_iff_OK"; |
360 qed "ok_iff_OK"; |