equal
deleted
inserted
replaced
336 using the given theorems, which should normally be introduction 
336 using the given theorems, which should normally be introduction 
337 rules. The tactic resolves a rule's conclusion with subgoal \isa{i}, replacing it by the corresponding versions of the rule's 
337 rules. The tactic resolves a rule's conclusion with subgoal \isa{i}, replacing it by the corresponding versions of the rule's 
338 premises. 
338 premises. 
339 
339 
340 \item \verberesolve_tac~\isa{thms\ i} performs elimresolution 
340 \item \verberesolve_tac~\isa{thms\ i} performs elimresolution 
341 with the given theorems, which should normally be elimination rules. 
341 with the given theorems, which are normally be elimination rules. 

342 

343 Note that \verberesolve_tac [asm_rl] is equivalent to \verbassume_tac, which facilitates mixing of assumption steps with 

344 genuine eliminations. 
342 
345 
343 \item \verbdresolve_tac~\isa{thms\ i} performs 
346 \item \verbdresolve_tac~\isa{thms\ i} performs 
344 destructresolution with the given theorems, which should normally 
347 destructresolution with the given theorems, which should normally 
345 be destruction rules. This replaces an assumption by the result of 
348 be destruction rules. This replaces an assumption by the result of 
346 applying one of the rules. 
349 applying one of the rules. 