| changeset 22148 | 3b99944136ef |
| parent 22141 | a91334ece12a |
| child 22153 | 649e1d769e15 |
--- a/src/HOL/ex/Binary.thy Sun Jan 21 16:43:46 2007 +0100 +++ b/src/HOL/ex/Binary.thy Sun Jan 21 16:43:47 2007 +0100 @@ -127,7 +127,7 @@ val plus = nat_op "HOL.plus"; val mult = nat_op "HOL.times"; - fun prove ctxt prop = (* FIXME avoid re-certification *) + fun prove ctxt prop = Goal.prove ctxt [] [] prop (fn _ => ALLGOALS (full_simp_tac binary_ss));