Cambridge University Press 1.1 Time Clock User Manual


  Open as PDF
of 116
 
86 CHAPTER 10. TACTICS
#let WISHNU = prove
(‘(?!x. x=f(g x)) = (?!y. y=g(f y))‘,
MESON_TAC[]);;
WISHNU : thm = |- (?!x. x = f (g x)) = (?!y. y = g (f y))
The tactic accepts a list of theorems to use in the proof. ASM MESON TAC also
uses the assumptions of the goal.
 previous next