src/HOL/IMPP/Com.ML
changeset 17477 ceb42ea2f223
parent 13911 f5c3750292f5
     1.1 --- a/src/HOL/IMPP/Com.ML	Sat Sep 17 19:17:35 2005 +0200
     1.2 +++ b/src/HOL/IMPP/Com.ML	Sat Sep 17 20:14:30 2005 +0200
     1.3 @@ -1,3 +1,5 @@
     1.4 +(* $Id$ *)
     1.5 +
     1.6  val make_imp_tac = EVERY'[rtac mp, fn i => atac (i+1), etac thin_rl];
     1.7  
     1.8  Goalw [body_def] "finite (dom body)";
     1.9 @@ -9,9 +11,4 @@
    1.10  by (Fast_tac 1);
    1.11  qed "WT_bodiesD";
    1.12  
    1.13 -val WTs_elim_cases = map WTs.mk_cases
    1.14 -   ["WT SKIP", "WT (X:==a)", "WT (LOCAL Y:=a IN c)", 
    1.15 -    "WT (c1;;c2)","WT (IF b THEN c1 ELSE c2)", "WT (WHILE b DO c)",
    1.16 -    "WT (BODY P)", "WT (X:=CALL P(a))"];
    1.17 -
    1.18  AddSEs WTs_elim_cases;