| changeset 10138 | 412a3ced6efd |
| parent 10042 | 7164dc0d24d8 |
| child 10212 | 33fe2d701ddd |
--- a/src/HOL/MicroJava/J/JBasis.ML Tue Oct 03 18:40:25 2000 +0200 +++ b/src/HOL/MicroJava/J/JBasis.ML Tue Oct 03 18:44:19 2000 +0200 @@ -140,7 +140,7 @@ (* More about Maps *) -val override_SomeD = prove_goalw thy [override_def] "(s \\<oplus> t) k = Some x ==> \ +val override_SomeD = prove_goalw thy [override_def] "(s ++ t) k = Some x ==> \ \ t k = Some x | t k = None \\<and> s k = Some x" (fn prems => [ cut_facts_tac prems 1, case_tac "\\<exists>x. t k = Some x" 1,