equal
deleted
inserted
replaced
66 example). The tactics @{ML_ind etac in Tactic}, @{ML_ind rtac in Tactic} and |
66 example). The tactics @{ML_ind etac in Tactic}, @{ML_ind rtac in Tactic} and |
67 @{ML_ind atac in Tactic} in the code above correspond roughly to @{text |
67 @{ML_ind atac in Tactic} in the code above correspond roughly to @{text |
68 erule}, @{text rule} and @{text assumption}, respectively. The combinator |
68 erule}, @{text rule} and @{text assumption}, respectively. The combinator |
69 @{ML THEN} strings the tactics together. |
69 @{ML THEN} strings the tactics together. |
70 |
70 |
|
71 TBD: Write something about @{ML_ind prove_multi in Goal}. |
|
72 |
71 \begin{readmore} |
73 \begin{readmore} |
72 To learn more about the function @{ML_ind prove in Goal} see |
74 To learn more about the function @{ML_ind prove in Goal} see |
73 \isccite{sec:results} and the file @{ML_file "Pure/goal.ML"}. See @{ML_file |
75 \isccite{sec:results} and the file @{ML_file "Pure/goal.ML"}. See @{ML_file |
74 "Pure/tactic.ML"} and @{ML_file "Pure/tactical.ML"} for the code of basic |
76 "Pure/tactic.ML"} and @{ML_file "Pure/tactical.ML"} for the code of basic |
75 tactics and tactic combinators; see also Chapters 3 and 4 in the old |
77 tactics and tactic combinators; see also Chapters 3 and 4 in the old |