equal
deleted
inserted
replaced
34 in case of problems. Sometimes subsequent calls to the classical |
34 in case of problems. Sometimes subsequent calls to the classical |
35 reasoner will fail because a preceeding call to the simplifier too |
35 reasoner will fail because a preceeding call to the simplifier too |
36 eagerly simplified the goal, e.g. deleted redundant premises. |
36 eagerly simplified the goal, e.g. deleted redundant premises. |
37 |
37 |
38 - The simplifier trace now shows the names of the applied rewrite rules |
38 - The simplifier trace now shows the names of the applied rewrite rules |
|
39 |
|
40 - You can limit the number of recursive invocations of the simplifier |
|
41 during conditional rewriting (where the simplifie tries to solve the |
|
42 conditions before applying the rewrite rule): |
|
43 ML "simp_depth_limit := n" |
|
44 where n is an integer. Thus you can force termination where previously |
|
45 the simplifier would diverge. |
|
46 |
39 |
47 |
40 * Pure: New flag for triggering if the overall goal of a proof state should |
48 * Pure: New flag for triggering if the overall goal of a proof state should |
41 be printed: |
49 be printed: |
42 PG menu: Isabelle/Isar -> Settigs -> Show Main Goal |
50 PG menu: Isabelle/Isar -> Settigs -> Show Main Goal |
43 (ML: Proof.show_main_goal). |
51 (ML: Proof.show_main_goal). |