summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

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. |