Mercurial Mercurial > wneuper > isa / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/Tools/isac/Interpret/script.sml
branchdecompose-isar
changeset 42023 927cb6806af1
parent 42018 11cf93cd02c6
child 42082 2556b7865f9b
equal deleted inserted replaced
42022:d08ea90c6f43 42023:927cb6806af1 
  1530               else nstep_up thy ptp sc E l Skip_ a v of
 
  1530               else nstep_up thy ptp sc E l Skip_ a v of
 
  1531             Skip (v, _) =>                                            (*finished*)
 
  1531             Skip (v, _) =>                                            (*finished*)
 
  1532               (case par_pbl_det pt p of
 
  1532               (case par_pbl_det pt p of
 
  1533 	               (true, p', _) => 
  1533 	               (true, p', _) => 
  1534 	                  let val (_,pblID,_) = get_obj g_spec pt p';
 
  1534 	                  let val (_,pblID,_) = get_obj g_spec pt p';
 
  1535 	                  in (Check_Postcond' (pblID, (v, [(*WN030608 NO asms???*)])), 
  1535 	                  in (Check_Postcond' (pblID, (v, [(*assigned in next step*)])), 
  1536 	                    (e_istate, ctxt), (v,s)) 
  1536 	                    (e_istate, ctxt), (v,s)) 
  1537                     end
 
  1537                     end
 
  1538 	             | (_, p', rls') => 
  1538 	             | (_, p', rls') => 
  1539                    (End_Detail' (e_term,[])(*8.6.03*), (e_istate, ctxt), (v,s)))
 
  1539                    (End_Detail' (e_term,[])(*8.6.03*), (e_istate, ctxt), (v,s)))
 
  1540          | Napp _ => (Empty_Tac_, (e_istate, ctxt), (e_term, Sundef)) (*helpless*)
 
  1540          | Napp _ => (Empty_Tac_, (e_istate, ctxt), (e_term, Sundef)) (*helpless*)
wneuper/isa