--- a/Nominal/Nominal2_FCB.thy	Tue Jul 05 04:23:33 2011 +0200
+++ b/Nominal/Nominal2_FCB.thy	Tue Jul 05 15:00:41 2011 +0200
@@ -3,6 +3,24 @@
 begin
 
 
+text {*
+  A tactic which solves all trivial cases in function 
+  definitions, and leaves the others unchanged.
+*}
+
+ML {*
+val all_trivials : (Proof.context -> Method.method) context_parser =
+Scan.succeed (fn ctxt =>
+ let
+   val tac = TRYALL (SOLVED' (full_simp_tac (simpset_of ctxt)))
+ in 
+   Method.SIMPLE_METHOD' (K tac)
+ end)
+*}
+
+method_setup all_trivials = {* all_trivials *} {* solves trivial goals *}
+
+
 lemma Abs_lst1_fcb:
   fixes x y :: "'a :: at_base"
     and S T :: "'b :: fs"