File Term.ML

open Term;

bind_thms ("is_stmt_rews", sum3_instantiate is_stmt_def);
Addsimps is_stmt_rews;

Goalw [is_stmt_def] "is_stmt t \<Longrightarrow> \<exists>c. t=In1r c";
b y atac 1;
qed "is_stmtD";