equal
deleted
inserted
replaced
25 begin |
25 begin |
26 note [[show_main_goal = true]] |
26 note [[show_main_goal = true]] |
27 end |
27 end |
28 (*<*)end(*>*) |
28 (*<*)end(*>*) |
29 |
29 |
30 text \<open>For historical reasons, some tools cannot take the full proof |
30 text \<open> |
31 context into account and merely refer to the background theory. |
|
32 This is accommodated by configuration options being declared as |
|
33 ``global'', which may not be changed within a local context. |
|
34 |
|
35 \begin{matharray}{rcll} |
31 \begin{matharray}{rcll} |
36 @{command_def "print_options"} & : & @{text "context \<rightarrow>"} \\ |
32 @{command_def "print_options"} & : & @{text "context \<rightarrow>"} \\ |
37 \end{matharray} |
33 \end{matharray} |
38 |
34 |
39 @{rail \<open> |
35 @{rail \<open> |