98 @{index_ML fold_goals_tac: "Proof.context -> thm list -> tactic"} \\ |
98 @{index_ML fold_goals_tac: "Proof.context -> thm list -> tactic"} \\ |
99 \end{mldecls} |
99 \end{mldecls} |
100 |
100 |
101 \begin{description} |
101 \begin{description} |
102 |
102 |
103 \item @{ML rewrite_rule}~@{text "ctxt rules thm"} rewrites the whole |
103 \<^descr> @{ML rewrite_rule}~@{text "ctxt rules thm"} rewrites the whole |
104 theorem by the given rules. |
104 theorem by the given rules. |
105 |
105 |
106 \item @{ML rewrite_goals_rule}~@{text "ctxt rules thm"} rewrites the |
106 \<^descr> @{ML rewrite_goals_rule}~@{text "ctxt rules thm"} rewrites the |
107 outer premises of the given theorem. Interpreting the same as a |
107 outer premises of the given theorem. Interpreting the same as a |
108 goal state (\secref{sec:tactical-goals}) it means to rewrite all |
108 goal state (\secref{sec:tactical-goals}) it means to rewrite all |
109 subgoals (in the same manner as @{ML rewrite_goals_tac}). |
109 subgoals (in the same manner as @{ML rewrite_goals_tac}). |
110 |
110 |
111 \item @{ML rewrite_goal_tac}~@{text "ctxt rules i"} rewrites subgoal |
111 \<^descr> @{ML rewrite_goal_tac}~@{text "ctxt rules i"} rewrites subgoal |
112 @{text "i"} by the given rewrite rules. |
112 @{text "i"} by the given rewrite rules. |
113 |
113 |
114 \item @{ML rewrite_goals_tac}~@{text "ctxt rules"} rewrites all subgoals |
114 \<^descr> @{ML rewrite_goals_tac}~@{text "ctxt rules"} rewrites all subgoals |
115 by the given rewrite rules. |
115 by the given rewrite rules. |
116 |
116 |
117 \item @{ML fold_goals_tac}~@{text "ctxt rules"} essentially uses @{ML |
117 \<^descr> @{ML fold_goals_tac}~@{text "ctxt rules"} essentially uses @{ML |
118 rewrite_goals_tac} with the symmetric form of each member of @{text |
118 rewrite_goals_tac} with the symmetric form of each member of @{text |
119 "rules"}, re-ordered to fold longer expression first. This supports |
119 "rules"}, re-ordered to fold longer expression first. This supports |
120 to idea to fold primitive definitions that appear in expended form |
120 to idea to fold primitive definitions that appear in expended form |
121 in the proof state. |
121 in the proof state. |
122 |
122 |