src/HOL/Statespace/state_fun.ML
changeset 36148 4ddcc2b07891
parent 35999 e031755609cf
child 36945 9bec62c10714
equal deleted inserted replaced
36147:b43b22f63665 36148:4ddcc2b07891
   191                let val ((c,cT),fs,(d,dT)) = split_list (the (AList.lookup (op aconv) comps n))
   191                let val ((c,cT),fs,(d,dT)) = split_list (the (AList.lookup (op aconv) comps n))
   192                in ((c,cT),fst (mk_comps fs),(d,dT)) end;
   192                in ((c,cT),fst (mk_comps fs),(d,dT)) end;
   193 
   193 
   194              (* mk_updterm returns 
   194              (* mk_updterm returns 
   195               *  - (orig-term-skeleton,simplified-term-skeleton, vars, b)
   195               *  - (orig-term-skeleton,simplified-term-skeleton, vars, b)
   196               *     where boolean b tells if a simplification has occured.
   196               *     where boolean b tells if a simplification has occurred.
   197                     "orig-term-skeleton = simplified-term-skeleton" is
   197                     "orig-term-skeleton = simplified-term-skeleton" is
   198               *     the desired simplification rule.
   198               *     the desired simplification rule.
   199               * The algorithm first walks down the updates to the seed-state while
   199               * The algorithm first walks down the updates to the seed-state while
   200               * memorising the updates in the already-table. While walking up the
   200               * memorising the updates in the already-table. While walking up the
   201               * updates again, the optimised term is constructed.
   201               * updates again, the optimised term is constructed.