equal
deleted
inserted
replaced
1004 apply clarify |
1004 apply clarify |
1005 apply (erule mp [THEN conseq12]) |
1005 apply (erule mp [THEN conseq12]) |
1006 apply (auto simp add: type_ok_def) |
1006 apply (auto simp add: type_ok_def) |
1007 done |
1007 done |
1008 |
1008 |
1009 ML {* bind_thms ("ax_Abrupts", sum3_instantiate @{context} @{thm ax_derivs.Abrupt}) *} |
1009 ML {* ML_Thms.bind_thms ("ax_Abrupts", sum3_instantiate @{context} @{thm ax_derivs.Abrupt}) *} |
1010 declare ax_Abrupts [intro!] |
1010 declare ax_Abrupts [intro!] |
1011 |
1011 |
1012 lemmas ax_Normal_cases = ax_cases [of _ _ _ normal] |
1012 lemmas ax_Normal_cases = ax_cases [of _ _ _ normal] |
1013 |
1013 |
1014 lemma ax_Skip [intro!]: "G,(A::'a triple set)\<turnstile>{P\<leftarrow>\<diamondsuit>} .Skip. {P::'a assn}" |
1014 lemma ax_Skip [intro!]: "G,(A::'a triple set)\<turnstile>{P\<leftarrow>\<diamondsuit>} .Skip. {P::'a assn}" |