equal
deleted
inserted
replaced
10 Addsimps [obj_ty_def2]; |
10 Addsimps [obj_ty_def2]; |
11 |
11 |
12 val new_AddrD = prove_goalw thy [new_Addr_def] |
12 val new_AddrD = prove_goalw thy [new_Addr_def] |
13 "\\<And>X. (a,x) = new_Addr h \\<Longrightarrow> h a = None \\<and> x = None | x = Some OutOfMemory" (K[ |
13 "\\<And>X. (a,x) = new_Addr h \\<Longrightarrow> h a = None \\<and> x = None | x = Some OutOfMemory" (K[ |
14 asm_full_simp_tac (simpset() addsimps [Pair_fst_snd_eq,select_split]) 1, |
14 asm_full_simp_tac (simpset() addsimps [Pair_fst_snd_eq,select_split]) 1, |
15 rtac selectI 1, |
15 rtac someI 1, |
16 rtac disjI2 1, |
16 rtac disjI2 1, |
17 res_inst_tac [("r","snd (a,Some OutOfMemory)")] trans 1, |
17 res_inst_tac [("r","snd (a,Some OutOfMemory)")] trans 1, |
18 Auto_tac ]); |
18 Auto_tac ]); |
19 |
19 |
20 val raise_if_True = prove_goalw thy [raise_if_def] |
20 val raise_if_True = prove_goalw thy [raise_if_def] |