equal
deleted
inserted
replaced
42 conditions before applying the rewrite rule): |
42 conditions before applying the rewrite rule): |
43 ML "simp_depth_limit := n" |
43 ML "simp_depth_limit := n" |
44 where n is an integer. Thus you can force termination where previously |
44 where n is an integer. Thus you can force termination where previously |
45 the simplifier would diverge. |
45 the simplifier would diverge. |
46 |
46 |
|
47 - Accepts free variables as head terms in congruence rules. Useful in Isar. |
47 |
48 |
48 * Pure: New flag for triggering if the overall goal of a proof state should |
49 * Pure: New flag for triggering if the overall goal of a proof state should |
49 be printed: |
50 be printed: |
50 PG menu: Isabelle/Isar -> Settigs -> Show Main Goal |
51 PG menu: Isabelle/Isar -> Settings -> Show Main Goal |
51 (ML: Proof.show_main_goal). |
52 (ML: Proof.show_main_goal). |
52 |
53 |
53 * Pure: You can find all matching introduction rules for subgoal 1, i.e. all |
54 * Pure: You can find all matching introduction rules for subgoal 1, i.e. all |
54 rules whose conclusion matches subgoal 1: |
55 rules whose conclusion matches subgoal 1: |
55 PG menu: Isabelle/Isar -> Show me -> matching rules |
56 PG menu: Isabelle/Isar -> Show me -> matching rules |