src/HOL/Lex/AutoProj.ML

match_bind(_i): 'as' patterns;
assume, theorem, show etc.: propp;
tuned qed msg;

(*  Title:      HOL/Lex/AutoProj.ML
    ID:         $Id$
    Author:     Tobias Nipkow
    Copyright   1998 TUM
*)

Goalw [start_def] "start(q,d,f) = q";
by (Simp_tac 1);
qed "start_conv";

Goalw [next_def] "next(q,d,f) = d";
by (Simp_tac 1);
qed "next_conv";

Goalw [fin_def] "fin(q,d,f) = f";
by (Simp_tac 1);
qed "fin_conv";

Addsimps [start_conv,next_conv,fin_conv];