# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1309870841 -7200
# Node ID d9c3cc271e628710989ca29a9a77f75f5c0a29a9
# Parent  70bbd18ad19479c310466be74effcec1183e0c0f
added a tactic "all_trivials" which simplifies all trivial constructor cases and leaves the others untouched.

diff -r 70bbd18ad194 -r d9c3cc271e62 Nominal/Nominal2_FCB.thy
--- 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"