equal
deleted
inserted
replaced
241 (* rewrite rule to push universal quantification through box: |
241 (* rewrite rule to push universal quantification through box: |
242 (sigma |= [](! x. F x)) = (! x. (sigma |= []F x)) |
242 (sigma |= [](! x. F x)) = (! x. (sigma |= []F x)) |
243 *) |
243 *) |
244 bind_thm("all_box", standard((temp_unlift allT) RS sym)); |
244 bind_thm("all_box", standard((temp_unlift allT) RS sym)); |
245 |
245 |
|
246 bind_thm ("contrapos_np", thm "contrapos_np"); |
246 |
247 |
247 Goal "|- (<>(F | G)) = (<>F | <>G)"; |
248 Goal "|- (<>(F | G)) = (<>F | <>G)"; |
248 by (auto_tac (temp_css addsimps2 [dmd_def,split_box_conj])); |
249 by (auto_tac (temp_css addsimps2 [dmd_def,split_box_conj])); |
249 by (ALLGOALS (EVERY' [etac contrapos_np, |
250 by (ALLGOALS (EVERY' [etac contrapos_np, |
250 merge_box_tac, |
251 merge_box_tac, |