doc-src/Tutorial/Datatype/tidproof.ML

Streamlined proofs of instances of Separation

Goal "subst  Var t  = (t ::('a,'b)term)  & \
\     substs Var ts = (ts::('a,'b)term list)";
by(induct_tac "t ts" 1);
by(Auto_tac);