47 header -- minor INCOMPATIBILITY for user-defined commands. Allow new |
47 header -- minor INCOMPATIBILITY for user-defined commands. Allow new |
48 commands to be used in the same theory where defined. |
48 commands to be used in the same theory where defined. |
49 |
49 |
50 |
50 |
51 *** Pure *** |
51 *** Pure *** |
|
52 |
|
53 * Auxiliary contexts indicate block structure for specifications with |
|
54 additional parameters and assumptions. Such unnamed contexts may be |
|
55 nested within other targets, like 'theory', 'locale', 'class', |
|
56 'instantiation' etc. Results from the local context are generalized |
|
57 accordingly and applied to the enclosing target context. Example: |
|
58 |
|
59 context |
|
60 fixes x y z :: 'a |
|
61 assumes xy: "x = y" and yz: "y = z" |
|
62 begin |
|
63 |
|
64 lemma my_trans: "x = z" using xy yz by simp |
|
65 |
|
66 end |
|
67 |
|
68 thm my_trans |
|
69 |
|
70 The most basic application is to factor-out context elements of |
|
71 several fixes/assumes/shows theorem statements, e.g. see |
|
72 ~~/src/HOL/Isar_Examples/Group_Context.thy |
|
73 |
|
74 Any other local theory specification element works within the "context |
|
75 ... begin ... end" block as well. |
52 |
76 |
53 * Rule composition via attribute "OF" (or ML functions OF/MRS) is more |
77 * Rule composition via attribute "OF" (or ML functions OF/MRS) is more |
54 tolerant against multiple unifiers, as long as the final result is |
78 tolerant against multiple unifiers, as long as the final result is |
55 unique. (As before, rules are composed in canonical right-to-left |
79 unique. (As before, rules are composed in canonical right-to-left |
56 order to accommodate newly introduced premises.) |
80 order to accommodate newly introduced premises.) |