diff -r 8732ff59068b -r c6db12ddb60c Nominal/Tacs.thy
--- a/Nominal/Tacs.thy	Wed May 26 15:37:56 2010 +0200
+++ b/Nominal/Tacs.thy	Thu May 27 18:37:52 2010 +0200
@@ -17,6 +17,17 @@
 end
 *}
 
+ML {*
+fun mk_conjl props =
+  fold (fn a => fn b =>
+    if a = @{term True} then b else
+    if b = @{term True} then a else
+    HOLogic.mk_conj (a, b)) (rev props) @{term True};
+*}
+
+ML {*
+val split_conj_tac = REPEAT o etac conjE THEN' TRY o REPEAT_ALL_NEW (CHANGED o rtac conjI)
+*}
 
 
 ML {*