equal
deleted
inserted
replaced
319 apply(auto)[1] |
319 apply(auto)[1] |
320 apply (metis Prf.intros(4)) |
320 apply (metis Prf.intros(4)) |
321 apply(erule Prf.cases) |
321 apply(erule Prf.cases) |
322 apply(simp_all)[5] |
322 apply(simp_all)[5] |
323 apply (metis ValOrd.intros) |
323 apply (metis ValOrd.intros) |
324 apply(simp add: POSIX_def) |
324 apply(simp) |
325 apply(auto)[1] |
325 apply(auto)[1] |
326 apply(simp add: POSIX_def) |
326 apply(simp add: POSIX_def) |
327 apply(auto)[1] |
327 apply(auto)[1] |
328 apply (metis mkeps.simps(2) mkeps_nullable nullable.simps(5)) |
328 apply (metis mkeps.simps(2) mkeps_nullable nullable.simps(5)) |
329 apply(rotate_tac 6) |
329 apply(rotate_tac 6) |