equal
deleted
inserted
replaced
971 apply (rule impI) |
971 apply (rule impI) |
972 apply (rule seq.take_lemmas) |
972 apply (rule seq.take_lemmas) |
973 apply (rule mp) |
973 apply (rule mp) |
974 prefer 2 apply assumption |
974 prefer 2 apply assumption |
975 apply (rule_tac x="x" in spec) |
975 apply (rule_tac x="x" in spec) |
976 apply (rule nat_induct) |
976 apply (rule nat.induct) |
977 apply simp |
977 apply simp |
978 apply (rule allI) |
978 apply (rule allI) |
979 apply (case_tac "Forall Q xa") |
979 apply (case_tac "Forall Q xa") |
980 apply (force intro!: seq_take_lemma [THEN iffD2, THEN spec]) |
980 apply (force intro!: seq_take_lemma [THEN iffD2, THEN spec]) |
981 apply (auto dest!: divide_Seq3) |
981 apply (auto dest!: divide_Seq3) |
1014 apply (rule impI) |
1014 apply (rule impI) |
1015 apply (rule seq.take_lemmas) |
1015 apply (rule seq.take_lemmas) |
1016 apply (rule mp) |
1016 apply (rule mp) |
1017 prefer 2 apply assumption |
1017 prefer 2 apply assumption |
1018 apply (rule_tac x="x" in spec) |
1018 apply (rule_tac x="x" in spec) |
1019 apply (rule nat_induct) |
1019 apply (rule nat.induct) |
1020 apply simp |
1020 apply simp |
1021 apply (rule allI) |
1021 apply (rule allI) |
1022 apply (rule_tac x="xa" in Seq_cases) |
1022 apply (rule_tac x="xa" in Seq_cases) |
1023 apply simp_all |
1023 apply simp_all |
1024 done |
1024 done |