equal
deleted
inserted
replaced
355 |
355 |
356 * Proper context for basic Simplifier operations: rewrite_rule, |
356 * Proper context for basic Simplifier operations: rewrite_rule, |
357 rewrite_goals_rule, rewrite_goals_tac etc. INCOMPATIBILITY, need to |
357 rewrite_goals_rule, rewrite_goals_tac etc. INCOMPATIBILITY, need to |
358 pass runtime Proof.context (and ensure that the simplified entity |
358 pass runtime Proof.context (and ensure that the simplified entity |
359 actually belongs to it). |
359 actually belongs to it). |
|
360 |
|
361 * Subtle change of semantics of Thm.eq_thm: theory stamps are not |
|
362 compared (according to Thm.thm_ord), but assumed to be covered by the |
|
363 current background theory. Thus equivalent data produced in different |
|
364 branches of the theory graph usually coincides (e.g. relevant for |
|
365 theory merge). Note that the softer Thm.eq_thm_prop is often more |
|
366 appropriate than Thm.eq_thm. |
360 |
367 |
361 |
368 |
362 *** System *** |
369 *** System *** |
363 |
370 |
364 * Simplified "isabelle display" tool. Settings variables DVI_VIEWER |
371 * Simplified "isabelle display" tool. Settings variables DVI_VIEWER |