| changeset 26480 | 544cef16045b |
| parent 26342 | 0f65fa163304 |
| child 27226 | 5a3e5e46d977 |
--- a/src/HOL/Bali/AxSem.thy Sat Mar 29 19:13:58 2008 +0100 +++ b/src/HOL/Bali/AxSem.thy Sat Mar 29 19:14:00 2008 +0100 @@ -1013,7 +1013,7 @@ apply (auto simp add: type_ok_def) done -ML_setup {* bind_thms ("ax_Abrupts", sum3_instantiate @{thm ax_derivs.Abrupt}) *} +ML {* bind_thms ("ax_Abrupts", sum3_instantiate @{thm ax_derivs.Abrupt}) *} declare ax_Abrupts [intro!] lemmas ax_Normal_cases = ax_cases [of _ _ _ normal]