# HG changeset patch
# User boehmes
# Date 1292404368 -3600
# Node ID bb2fa5c13d1a5774bf9fcbe79376e100f8ccccb4
# Parent  2ea84c8535c6c3ba48f202fe8096e28765f64d14
always add pair rules and function update rules automatically (Boogie provides pairs and function update as built-in concepts and does not generate background axioms for them)

diff -r 2ea84c8535c6 -r bb2fa5c13d1a src/HOL/Boogie/Tools/boogie_tactics.ML
--- a/src/HOL/Boogie/Tools/boogie_tactics.ML	Wed Dec 15 10:12:44 2010 +0100
+++ b/src/HOL/Boogie/Tools/boogie_tactics.ML	Wed Dec 15 10:12:48 2010 +0100
@@ -28,9 +28,13 @@
   let val unfold = Conv.rewrs_conv label_eqs
   in CONVERSION (Conv.top_sweep_conv (K unfold) ctxt) end
 
+val boogie_rules =
+  [@{thm fst_conv}, @{thm snd_conv}, @{thm pair_collapse}] @
+  [@{thm fun_upd_same}, @{thm fun_upd_apply}]
+
 fun boogie_tac ctxt rules =
   unfold_labels_tac ctxt
-  THEN' SMT_Solver.smt_tac ctxt (Boogie_Axioms.get ctxt @ rules)
+  THEN' SMT_Solver.smt_tac ctxt (Boogie_Axioms.get ctxt @ boogie_rules @ rules)
 
 fun boogie_all_tac ctxt rules =
   PARALLEL_GOALS (HEADGOAL (boogie_tac ctxt rules))