src/HOL/IMPP/Com.ML
author wenzelm
Sat, 17 Sep 2005 20:14:30 +0200
changeset 17477 ceb42ea2f223
parent 13911 f5c3750292f5
permissions -rw-r--r--
converted to Isar theory format;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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;