equal
deleted
inserted
replaced
122 qed |
122 qed |
123 qed |
123 qed |
124 qed |
124 qed |
125 qed |
125 qed |
126 |
126 |
127 locale red_extend_highest_gen = extend_highest_gen + |
127 (* locale red_extend_highest_gen = extend_highest_gen + |
128 fixes i::nat |
128 fixes i::nat |
129 |
129 *) |
|
130 |
|
131 (* |
130 sublocale red_extend_highest_gen < red_moment: extend_highest_gen "s" "th" "prio" "tm" "(moment i t)" |
132 sublocale red_extend_highest_gen < red_moment: extend_highest_gen "s" "th" "prio" "tm" "(moment i t)" |
131 apply (insert extend_highest_gen_axioms, subst (asm) (1) moment_restm_s [of i t, symmetric]) |
133 apply (insert extend_highest_gen_axioms, subst (asm) (1) moment_restm_s [of i t, symmetric]) |
132 apply (unfold extend_highest_gen_def extend_highest_gen_axioms_def, clarsimp) |
134 apply (unfold extend_highest_gen_def extend_highest_gen_axioms_def, clarsimp) |
133 by (unfold highest_gen_def, auto dest:step_back_vt_app) |
135 by (unfold highest_gen_def, auto dest:step_back_vt_app) |
|
136 *) |
134 |
137 |
135 context extend_highest_gen |
138 context extend_highest_gen |
136 begin |
139 begin |
137 |
140 |
138 lemma ind [consumes 0, case_names Nil Cons, induct type]: |
141 lemma ind [consumes 0, case_names Nil Cons, induct type]: |
788 next |
791 next |
789 case False |
792 case False |
790 thus ?thesis using th_blockedE by auto |
793 thus ?thesis using th_blockedE by auto |
791 qed |
794 qed |
792 |
795 |
|
796 |
793 end |
797 end |
794 end |
798 end |