changeset 9970 | dfe4747c8318 |
parent 9385 | 6e1ac1629ac7 |
child 10042 | 7164dc0d24d8 |
--- a/src/HOL/MicroJava/J/State.ML Fri Sep 15 12:39:57 2000 +0200 +++ b/src/HOL/MicroJava/J/State.ML Fri Sep 15 15:30:50 2000 +0200 @@ -12,7 +12,7 @@ val new_AddrD = prove_goalw thy [new_Addr_def] "\\<And>X. (a,x) = new_Addr h \\<Longrightarrow> h a = None \\<and> x = None | x = Some OutOfMemory" (K[ asm_full_simp_tac (simpset() addsimps [Pair_fst_snd_eq,select_split]) 1, - rtac selectI 1, + rtac someI 1, rtac disjI2 1, res_inst_tac [("r","snd (a,Some OutOfMemory)")] trans 1, Auto_tac ]);