equal
deleted
inserted
replaced
12 state using tactics. This is similar to the \isacommand{apply}-style |
12 state using tactics. This is similar to the \isacommand{apply}-style |
13 reasoning at the user-level, where goals are modified in a sequence of proof |
13 reasoning at the user-level, where goals are modified in a sequence of proof |
14 steps until all of them are solved. However, there are also more structured |
14 steps until all of them are solved. However, there are also more structured |
15 operations available on the ML-level that help with the handling of |
15 operations available on the ML-level that help with the handling of |
16 variables and assumptions. |
16 variables and assumptions. |
17 |
|
18 *} |
17 *} |
19 |
18 |
20 |
19 |
21 section {* Basics of Reasoning with Tactics*} |
20 section {* Basics of Reasoning with Tactics*} |
22 |
21 |
1065 \begin{readmore} |
1064 \begin{readmore} |
1066 Most tactic combinators described in this section are defined in @{ML_file "Pure/tactical.ML"}. |
1065 Most tactic combinators described in this section are defined in @{ML_file "Pure/tactical.ML"}. |
1067 Some combinators for the purpose of proof search are implemented in @{ML_file "Pure/search.ML"}. |
1066 Some combinators for the purpose of proof search are implemented in @{ML_file "Pure/search.ML"}. |
1068 \end{readmore} |
1067 \end{readmore} |
1069 |
1068 |
|
1069 \begin{exercise}\label{ex:dyckhoff} |
|
1070 |
|
1071 \end{exercise} |
|
1072 |
1070 *} |
1073 *} |
1071 |
1074 |
1072 section {* Simplifier Tactics *} |
1075 section {* Simplifier Tactics *} |
1073 |
1076 |
1074 text {* |
1077 text {* |