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

src/Pure/section_utils.ML

changeset 3536 | 8fb4150e2ad3 |

parent 2863 | d97f5f424b97 |

child 3934 | a9c8960e4da6 |

equal
deleted
inserted
replaced

3535:19bd6c8274c4 | 3536:8fb4150e2ad3 |
---|---|

25 fun assume_read thy a = assume (read_cterm (sign_of thy) (a,propT)); |
25 fun assume_read thy a = assume (read_cterm (sign_of thy) (a,propT)); |

26 |
26 |

27 (*Read a term from string "b", with expected type T*) |
27 (*Read a term from string "b", with expected type T*) |

28 fun readtm sign T b = |
28 fun readtm sign T b = |

29 read_cterm sign (b,T) |> term_of |
29 read_cterm sign (b,T) |> term_of |

30 handle ERROR => error ("The error above occurred for " ^ b); |
30 handle ERROR => error ("The error(s) above occurred for " ^ b); |

31 |
31 |

32 (*From HOL/ex/meson.ML: raises exception if no rules apply -- unlike RL*) |
32 (*From HOL/ex/meson.ML: raises exception if no rules apply -- unlike RL*) |

33 fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls)) |
33 fun tryres (th, rl::rls) = (th RS rl handle THM _ => tryres(th,rls)) |

34 | tryres (th, []) = raise THM("tryres", 0, [th]); |
34 | tryres (th, []) = raise THM("tryres", 0, [th]); |

35 |
35 |