equal
deleted
inserted
replaced
20 local definitions to terms of the target domain of an interpretation. |
20 local definitions to terms of the target domain of an interpretation. |
21 |
21 |
22 * Reactivated diagnositc command 'print_interps'. Use 'print_interps l' |
22 * Reactivated diagnositc command 'print_interps'. Use 'print_interps l' |
23 to print all interpretations of locale l in the theory. Interpretations |
23 to print all interpretations of locale l in the theory. Interpretations |
24 in proofs are not shown. |
24 in proofs are not shown. |
|
25 |
|
26 * Thoroughly revised locales tutorial. New section on conditional |
|
27 interpretation. |
25 |
28 |
26 |
29 |
27 *** HOL *** |
30 *** HOL *** |
28 |
31 |
29 * Most rules produced by inductive and datatype package |
32 * Most rules produced by inductive and datatype package |