equal
deleted
inserted
replaced
9 *) |
9 *) |
10 |
10 |
11 (*All but the fastest are ignored to reduce build time*) |
11 (*All but the fastest are ignored to reduce build time*) |
12 val even_hard_ones = false; |
12 val even_hard_ones = false; |
13 |
13 |
14 (*Product_Type.thy instead of HOL.thy regards arguments as tuples. |
14 fun prove (s,tac) = prove_goal (the_context ()) s (fn [] => [tac]); |
15 But Main.thy would allow clashes with many other constants*) |
|
16 fun prove (s,tac) = prove_goal Product_Type.thy s (fn [] => [tac]); |
|
17 |
15 |
18 fun prove_hard arg = if even_hard_ones then prove arg else TrueI; |
16 fun prove_hard arg = if even_hard_ones then prove arg else TrueI; |
19 |
17 |
20 set timing; |
18 set timing; |
21 |
19 |