| changeset 4446 | 097004a470fb |
| parent 4091 | 771b1f6422a8 |
| child 5068 | fb28eaa07e01 |
--- a/src/ZF/ex/Bin.ML Fri Dec 19 10:17:04 1997 +0100 +++ b/src/ZF/ex/Bin.ML Fri Dec 19 10:18:03 1997 +0100 @@ -384,7 +384,7 @@ (*** Examples of performing binary arithmetic by simplification ***) -proof_timing := true; +set proof_timing; (*All runtimes below are on a SPARCserver 10*) goal Bin.thy "#13 $+ #19 = #32";