equal
deleted
inserted
replaced
61 The operator @{ML [index] THEN} strings the tactics together. |
61 The operator @{ML [index] THEN} strings the tactics together. |
62 |
62 |
63 \begin{readmore} |
63 \begin{readmore} |
64 To learn more about the function @{ML [index] prove in Goal} see \isccite{sec:results} |
64 To learn more about the function @{ML [index] prove in Goal} see \isccite{sec:results} |
65 and the file @{ML_file "Pure/goal.ML"}. See @{ML_file |
65 and the file @{ML_file "Pure/goal.ML"}. See @{ML_file |
66 "Pure/tactic.ML"} and @{ML_file "Pure/tctical.ML"} for the code of basic |
66 "Pure/tactic.ML"} and @{ML_file "Pure/tactical.ML"} for the code of basic |
67 tactics and tactic combinators; see also Chapters 3 and 4 in the old |
67 tactics and tactic combinators; see also Chapters 3 and 4 in the old |
68 Isabelle Reference Manual, and Chapter 3 in the Isabelle/Isar Implementation Manual. |
68 Isabelle Reference Manual, and Chapter 3 in the Isabelle/Isar Implementation Manual. |
69 \end{readmore} |
69 \end{readmore} |
70 |
70 |
71 Note that in the code above we use antiquotations for referencing the theorems. Many theorems |
71 Note that in the code above we use antiquotations for referencing the theorems. Many theorems |
1056 will solve all trivial subgoals involving @{term True} or @{term "False"}. |
1056 will solve all trivial subgoals involving @{term True} or @{term "False"}. |
1057 |
1057 |
1058 (FIXME: say something about @{ML [index] COND} and COND') |
1058 (FIXME: say something about @{ML [index] COND} and COND') |
1059 |
1059 |
1060 \begin{readmore} |
1060 \begin{readmore} |
1061 Most tactic combinators described in this section are defined in @{ML_file "Pure/tctical.ML"}. |
1061 Most tactic combinators described in this section are defined in @{ML_file "Pure/tactical.ML"}. |
1062 Some combinators for the purpose of proof search are implemented in @{ML_file "Pure/search.ML"}. |
1062 Some combinators for the purpose of proof search are implemented in @{ML_file "Pure/search.ML"}. |
1063 \end{readmore} |
1063 \end{readmore} |
1064 |
1064 |
1065 *} |
1065 *} |
1066 |
1066 |