equal
deleted
inserted
replaced
1 \begin{isabelle}% |
1 % |
|
2 \begin{isabellebody}% |
2 % |
3 % |
3 \begin{isamarkuptext}% |
4 \begin{isamarkuptext}% |
4 By default, assumptions are part of the simplification process: they are used |
5 By default, assumptions are part of the simplification process: they are used |
5 as simplification rules and are simplified themselves. For example:% |
6 as simplification rules and are simplified themselves. For example:% |
6 \end{isamarkuptext}% |
7 \end{isamarkuptext}% |
42 problematic subgoal. |
43 problematic subgoal. |
43 |
44 |
44 Note that only one of the above options is allowed, and it must precede all |
45 Note that only one of the above options is allowed, and it must precede all |
45 other arguments.% |
46 other arguments.% |
46 \end{isamarkuptext}% |
47 \end{isamarkuptext}% |
47 \end{isabelle}% |
48 \end{isabellebody}% |
48 %%% Local Variables: |
49 %%% Local Variables: |
49 %%% mode: latex |
50 %%% mode: latex |
50 %%% TeX-master: "root" |
51 %%% TeX-master: "root" |
51 %%% End: |
52 %%% End: |