Step
*
of Lemma
atom-value-type
value-type(Atom)
BY
{ TACTIC:(ValueTypeAuto THEN Refine_callbyvalueAtom THEN Trivial) }
Latex:
Latex:
value-type(Atom)
By
Latex:
TACTIC:(ValueTypeAuto  THEN  Refine\_callbyvalueAtom  THEN  Trivial)
Home
Index