# HG changeset patch # User paulson # Date 864204942 -7200 # Node ID 4a3ab8d434519d9eb10c2443bbbb38fe923efa29 # Parent eca2a3634acde4576a9e61f7549941c449bf5f7c TFL induction rule is now curried diff -r eca2a3634acd -r 4a3ab8d43451 src/HOL/ex/Primes.ML --- 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);