equal
deleted
inserted
replaced
114 \<close> |
114 \<close> |
115 |
115 |
116 ML \<open> |
116 ML \<open> |
117 "artifically inject assumptions"; |
117 "artifically inject assumptions"; |
118 val (SOME (iform, cform), SOME (ires, cres)) = Ctree.get_obj Ctree.g_loc pt (fst p); |
118 val (SOME (iform, cform), SOME (ires, cres)) = Ctree.get_obj Ctree.g_loc pt (fst p); |
119 val ctxt = ContextC.insert_assumptions [TermC.str2term "x < sub_asm_out", |
119 val ctxt = ContextC.insert_assumptions [TermC.parse_test @{context} "x < sub_asm_out", |
120 TermC.str2term "a < sub_asm_local"] cres; |
120 TermC.parse_test @{context} "a < sub_asm_local"] cres; |
121 val pt = Ctree.update_loc' pt (fst p) (SOME (iform, cform), SOME (ires, ctxt)); |
121 val pt = Ctree.update_loc' pt (fst p) (SOME (iform, cform), SOME (ires, ctxt)); |
122 \<close> |
122 \<close> |
123 |
123 |
124 ML \<open> |
124 ML \<open> |
125 val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt; |
125 val (p,_,f,nxt,_,pt) = Test_Code.me nxt p [] pt; |