equal
deleted
inserted
replaced
104 "@{thm \"disjE\"}" |
104 "@{thm \"disjE\"}" |
105 "\<lbrakk>?P \<or> ?Q; ?P \<Longrightarrow> ?R; ?Q \<Longrightarrow> ?R\<rbrakk> \<Longrightarrow> ?R"} |
105 "\<lbrakk>?P \<or> ?Q; ?P \<Longrightarrow> ?R; ?Q \<Longrightarrow> ?R\<rbrakk> \<Longrightarrow> ?R"} |
106 |
106 |
107 because then the theorems are fixed statically at compile-time. |
107 because then the theorems are fixed statically at compile-time. |
108 |
108 |
|
109 \index{tactic@ {\tt\slshape{}tactic}} |
|
110 \index{raw\_tactic@ {\tt\slshape{}raw\_tactic}} |
109 During the development of automatic proof procedures, you will often find it |
111 During the development of automatic proof procedures, you will often find it |
110 necessary to test a tactic on examples. This can be conveniently done with |
112 necessary to test a tactic on examples. This can be conveniently done with |
111 the command \isacommand{apply}@{text "(tactic \<verbopen> \<dots> \<verbclose>)"}. |
113 the command \isacommand{apply}@{text "(tactic \<verbopen> \<dots> \<verbclose>)"}. |
112 Consider the following sequence of tactics |
114 Consider the following sequence of tactics |
113 |
115 |
128 done |
130 done |
129 |
131 |
130 text {* |
132 text {* |
131 By using @{text "tactic \<verbopen> \<dots> \<verbclose>"} you can call from the |
133 By using @{text "tactic \<verbopen> \<dots> \<verbclose>"} you can call from the |
132 user-level of Isabelle the tactic @{ML foo_tac} or |
134 user-level of Isabelle the tactic @{ML foo_tac} or |
133 any other function that returns a tactic. |
135 any other function that returns a tactic. There are some goal transformation |
|
136 that are performed by @{text "tactic"}. They can be avoided by using |
|
137 @{text "raw_tactic"} instead. |
134 |
138 |
135 The tactic @{ML foo_tac} is just a sequence of simple tactics stringed |
139 The tactic @{ML foo_tac} is just a sequence of simple tactics stringed |
136 together by @{ML THEN}. As can be seen, each simple tactic in @{ML foo_tac} |
140 together by @{ML THEN}. As can be seen, each simple tactic in @{ML foo_tac} |
137 has a hard-coded number that stands for the subgoal analysed by the |
141 has a hard-coded number that stands for the subgoal analysed by the |
138 tactic (@{text "1"} stands for the first, or top-most, subgoal). This hard-coding |
142 tactic (@{text "1"} stands for the first, or top-most, subgoal). This hard-coding |