summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson |

Wed, 21 May 1997 10:55:42 +0200 | |

changeset 3270 | 4a3ab8d43451 |

parent 3269 | eca2a3634acd |

child 3271 | b873969b05d3 |

TFL induction rule is now curried

--- a/src/HOL/ex/Primes.ML Wed May 21 10:55:21 1997 +0200 +++ b/src/HOL/ex/Primes.ML Wed May 21 10:55:42 1997 +0200 @@ -50,10 +50,7 @@ val tc = result(); val gcd_eq = tc RS hd gcd.rules; -val gcd_induct = tc RS gcd.induct - |> read_instantiate [("P","split Q")] - |> rewrite_rule [split RS eq_reflection] - |> standard; +val gcd_induct = tc RS gcd.induct; goal thy "gcd(m,0) = m"; by (rtac (gcd_eq RS trans) 1);