equal
deleted
inserted
replaced
39 text \<open> |
39 text \<open> |
40 Note that this function, in addition to a tactic, also takes a state \<open>st\<close> as argument and applies this state to the tactic (Line 4). The reason is that |
40 Note that this function, in addition to a tactic, also takes a state \<open>st\<close> as argument and applies this state to the tactic (Line 4). The reason is that |
41 tactics are lazy functions and you need to force them to run, otherwise the |
41 tactics are lazy functions and you need to force them to run, otherwise the |
42 timing will be meaningless. The simplifier tactic, amongst others, can be |
42 timing will be meaningless. The simplifier tactic, amongst others, can be |
43 forced to run by just applying the state to it. But ``fully'' lazy tactics, |
43 forced to run by just applying the state to it. But ``fully'' lazy tactics, |
44 such as @{ML "resolve_tac"}, need even more ``standing-on-ones-head'' to force |
44 such as @{ML \<open>resolve_tac\<close>}, need even more ``standing-on-ones-head'' to force |
45 them to run. |
45 them to run. |
46 |
46 |
47 The time between start and finish of the simplifier will be calculated |
47 The time between start and finish of the simplifier will be calculated |
48 as the end time minus the start time. An example of the |
48 as the end time minus the start time. An example of the |
49 wrapper is the proof |
49 wrapper is the proof |