isabelle: src/HOL/IMPP/Com.ML@1dc034c3df61 (annotated)

17477 ceb42ea2f223 converted to Isar theory format; wenzelm parents: 13911 diff changeset	1	(* $Id$ *)
ceb42ea2f223 converted to Isar theory format; wenzelm parents: 13911 diff changeset	2
8180 879280b50571 added forgotten definition of make_imp_tac oheimb parents: 8177 diff changeset	3	val make_imp_tac = EVERY'[rtac mp, fn i => atac (i+1), etac thin_rl];
879280b50571 added forgotten definition of make_imp_tac oheimb parents: 8177 diff changeset	4
8177 e59e93ad85eb added IMPP to HOL oheimb parents: diff changeset	5	Goalw [body_def] "finite (dom body)";
13911 f5c3750292f5 added thm"..." due to new Map.thy nipkow parents: 10962 diff changeset	6	by (rtac (thm"finite_dom_map_of") 1);
8177 e59e93ad85eb added IMPP to HOL oheimb parents: diff changeset	7	qed "finite_dom_body";
e59e93ad85eb added IMPP to HOL oheimb parents: diff changeset	8
e59e93ad85eb added IMPP to HOL oheimb parents: diff changeset	9	Goalw [WT_bodies_def, body_def] "[\| WT_bodies; body pn = Some b \|] ==> WT b";
13911 f5c3750292f5 added thm"..." due to new Map.thy nipkow parents: 10962 diff changeset	10	by (dtac (thm"map_of_SomeD") 1);
8177 e59e93ad85eb added IMPP to HOL oheimb parents: diff changeset	11	by (Fast_tac 1);
e59e93ad85eb added IMPP to HOL oheimb parents: diff changeset	12	qed "WT_bodiesD";
e59e93ad85eb added IMPP to HOL oheimb parents: diff changeset	13
e59e93ad85eb added IMPP to HOL oheimb parents: diff changeset	14	AddSEs WTs_elim_cases;