| changeset 62390 | 842917225d56 |
| parent 62042 | 6c6ccf573479 |
| child 63648 | f9f3006a5579 |
--- a/src/HOL/MicroJava/J/JTypeSafe.thy Tue Feb 23 15:37:18 2016 +0100 +++ b/src/HOL/MicroJava/J/JTypeSafe.thy Tue Feb 23 16:25:08 2016 +0100 @@ -171,7 +171,7 @@ -declare split_if [split del] +declare if_split [split del] declare fun_upd_apply [simp del] declare fun_upd_same [simp] declare wf_prog_ws_prog [simp]