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

src/HOL/Tools/TFL/casesplit.ML

changeset 32952 | aeb1e44fbc19 |

parent 32727 | 9072201cd69d |

child 36945 | 9bec62c10714 |

equal
deleted
inserted
replaced

32951:83392f9d303f | 32952:aeb1e44fbc19 |
---|---|

303 (* derive eqs, assuming strict, ie the rules have no assumptions = all |
303 (* derive eqs, assuming strict, ie the rules have no assumptions = all |

304 the well-foundness conditions have been solved. *) |
304 the well-foundness conditions have been solved. *) |

305 fun derive_init_eqs sgn rules eqs = |
305 fun derive_init_eqs sgn rules eqs = |

306 let |
306 let |

307 fun get_related_thms i = |
307 fun get_related_thms i = |

308 List.mapPartial ((fn (r, x) => if x = i then SOME r else NONE)); |
308 map_filter ((fn (r, x) => if x = i then SOME r else NONE)); |

309 fun add_eq (i, e) xs = |
309 fun add_eq (i, e) xs = |

310 (e, (get_related_thms i rules), i) :: xs |
310 (e, (get_related_thms i rules), i) :: xs |

311 fun solve_eq (th, [], i) = |
311 fun solve_eq (th, [], i) = |

312 error "derive_init_eqs: missing rules" |
312 error "derive_init_eqs: missing rules" |

313 | solve_eq (th, [a], i) = (a, i) |
313 | solve_eq (th, [a], i) = (a, i) |