author | nipkow |
Wed, 26 Jul 2000 19:42:19 +0200 | |
changeset 9447 | e5180c869772 |
parent 8259 | a8d2606f4921 |
child 10962 | cda180b1e2e0 |
permissions | -rw-r--r-- |
val make_imp_tac = EVERY'[rtac mp, fn i => atac (i+1), etac thin_rl]; Goalw [body_def] "finite (dom body)"; br finite_dom_map_of 1; qed "finite_dom_body"; Goalw [WT_bodies_def, body_def] "[| WT_bodies; body pn = Some b |] ==> WT b"; bd map_of_SomeD 1; by (Fast_tac 1); qed "WT_bodiesD"; val WTs_elim_cases = map WTs.mk_cases ["WT SKIP", "WT (X:==a)", "WT (LOCAL Y:=a IN c)", "WT (c1;;c2)","WT (IF b THEN c1 ELSE c2)", "WT (WHILE b DO c)", "WT (BODY P)", "WT (X:=CALL P(a))"]; AddSEs WTs_elim_cases;