equal
deleted
inserted
replaced
280 rules. The tactic resolves a rule's conclusion with subgoal @{text 
280 rules. The tactic resolves a rule's conclusion with subgoal @{text 
281 i}, replacing it by the corresponding versions of the rule's 
281 i}, replacing it by the corresponding versions of the rule's 
282 premises. 
282 premises. 
283 
283 
284 \item @{ML eresolve_tac}~@{text "thms i"} performs elimresolution 
284 \item @{ML eresolve_tac}~@{text "thms i"} performs elimresolution 
285 with the given theorems, which should normally be elimination rules. 
285 with the given theorems, which are normally be elimination rules. 

286 

287 Note that @{ML "eresolve_tac [asm_rl]"} is equivalent to @{ML 

288 assume_tac}, which facilitates mixing of assumption steps with 

289 genuine eliminations. 
286 
290 
287 \item @{ML dresolve_tac}~@{text "thms i"} performs 
291 \item @{ML dresolve_tac}~@{text "thms i"} performs 
288 destructresolution with the given theorems, which should normally 
292 destructresolution with the given theorems, which should normally 
289 be destruction rules. This replaces an assumption by the result of 
293 be destruction rules. This replaces an assumption by the result of 
290 applying one of the rules. 
294 applying one of the rules. 