| changeset 8442 | 96023903c2df |
| parent 8423 | 3c19160b6432 |
| child 8875 | ac86b3d44730 |
--- a/src/HOL/MicroJava/J/JTypeSafe.ML Mon Mar 13 15:42:19 2000 +0100 +++ b/src/HOL/MicroJava/J/JTypeSafe.ML Mon Mar 13 16:23:34 2000 +0100 @@ -284,7 +284,7 @@ (* Level 45 *) (* 1 Call *) -by( cases_tac "x" 1); +by( case_tac "x" 1); by( Clarsimp_tac 2); by( dtac exec_xcpt 2); by( Asm_full_simp_tac 2);