equal
deleted
inserted
replaced
398 apply(case_tac s) |
398 apply(case_tac s) |
399 apply(simp) |
399 apply(simp) |
400 apply(rule subset_trans) |
400 apply(rule subset_trans) |
401 thm pders_STAR |
401 thm pders_STAR |
402 apply(rule pders_STAR) |
402 apply(rule pders_STAR) |
403 apply(simp) |
403 apply(simp) |
404 apply(auto simp add: pders_Set_def)[1] |
404 apply(auto simp add: pders_Set_def)[1] |
|
405 (* rest of SEQ case *) |
405 apply(simp) |
406 apply(simp) |
406 apply(rule conjI) |
407 apply(rule conjI) |
407 apply blast |
408 apply blast |
408 apply(auto simp add: pders_Set_def)[1] |
409 apply(auto simp add: pders_Set_def)[1] |
409 done |
410 done |