# HG changeset patch
# User boehmes
# Date 1258369799 -3600
# Node ID ffc5176a91051d98d513ba039d8b90b6c62ce81e
# Parent  93a4a42603a7cecd2de05f4182ca4a5bb0345a94
further explosion of HOL-Boogie verification conditions

diff -r 93a4a42603a7 -r ffc5176a9105 src/HOL/Boogie/Tools/boogie_split.ML
--- a/src/HOL/Boogie/Tools/boogie_split.ML	Mon Nov 16 11:14:43 2009 +0100
+++ b/src/HOL/Boogie/Tools/boogie_split.ML	Mon Nov 16 12:09:59 2009 +0100
@@ -112,14 +112,17 @@
 (* splitting method *)
 
 local
-  val split_rules = [@{thm impI}, @{thm conjI}, @{thm TrueI}]
+  val intro_rules = [@{thm impI}, @{thm conjI}, @{thm TrueI}]
+  val elim_rules = [@{thm conjE}, @{thm TrueE}]
+  val split_tac = REPEAT_ALL_NEW
+    (Tactic.resolve_tac intro_rules ORELSE' Tactic.eresolve_tac elim_rules)
 
   fun ALL_GOALS false tac = ALLGOALS tac
     | ALL_GOALS true tac = PARALLEL_GOALS (HEADGOAL tac)
 
   fun prep_tac ctxt ((parallel, verbose), subs) facts =
     HEADGOAL (Method.insert_tac facts)
-    THEN HEADGOAL (REPEAT_ALL_NEW (Tactic.resolve_tac split_rules))
+    THEN HEADGOAL split_tac
     THEN unique_case_names (ProofContext.theory_of ctxt)
     THEN ALL_GOALS parallel (SUBGOAL (fn (t, i) =>
       TRY (sub_tactics_tac ctxt (verbose, subs) (case_name_of t) i)))