# HG changeset patch
# User wenzelm
# Date 1194633453 -3600
# Node ID 7f012f56efa38f854b185969476a88a6aa68cc03
# Parent  fbdfceb8de15840fb0778b9cd50ce7c4792d594f
tuned proofs -- avoid implicit prems;

diff -r fbdfceb8de15 -r 7f012f56efa3 src/HOL/Statespace/DistinctTreeProver.thy
--- a/src/HOL/Statespace/DistinctTreeProver.thy	Fri Nov 09 19:37:32 2007 +0100
+++ b/src/HOL/Statespace/DistinctTreeProver.thy	Fri Nov 09 19:37:33 2007 +0100
@@ -120,7 +120,7 @@
   case Tip thus ?case by simp
 next
   case (Node l y d r)
-  have del: "delete x (Node l y d r) = Some t'".
+  have del: "delete x (Node l y d r) = Some t'" by fact
   show ?case
   proof (cases "delete x l")
     case (Some l')
@@ -170,8 +170,8 @@
   case Tip thus ?case by simp
 next
   case (Node l y d r)
-  have del: "delete x (Node l y d r) = Some t'".
-  have "all_distinct (Node l y d r)".
+  have del: "delete x (Node l y d r) = Some t'" by fact
+  have "all_distinct (Node l y d r)" by fact
   then obtain
     dist_l: "all_distinct l" and
     dist_r: "all_distinct r" and
@@ -243,7 +243,7 @@
   case Tip thus ?case by simp
 next
   case (Node l y d r)
-  have del: "delete x (Node l y d r) = Some t'".
+  have del: "delete x (Node l y d r) = Some t'" by fact
   show ?case
   proof (cases "delete x l")
     case (Some l')
@@ -310,7 +310,7 @@
   case Tip thus ?case by simp
 next
   case (Node l x b r)
-  have sub: "subtract (Node l x b r) t\<^isub>2 = Some t".
+  have sub: "subtract (Node l x b r) t\<^isub>2 = Some t" by fact
   show ?case
   proof (cases "delete x t\<^isub>2")
     case (Some t\<^isub>2')
@@ -355,7 +355,7 @@
   case Tip thus ?case by simp
 next
   case (Node l x d r)
-  have sub: "subtract (Node l x d r) t\<^isub>2 = Some t".
+  have sub: "subtract (Node l x d r) t\<^isub>2 = Some t" by fact
   show ?case
   proof (cases "delete x t\<^isub>2")
     case (Some t\<^isub>2')
@@ -405,8 +405,8 @@
   case Tip thus ?case by simp
 next
   case (Node l x d r)
-  have sub: "subtract (Node l x d r) t\<^isub>2 = Some t".
-  have dist_t2: "all_distinct t\<^isub>2".
+  have sub: "subtract (Node l x d r) t\<^isub>2 = Some t" by fact
+  have dist_t2: "all_distinct t\<^isub>2" by fact
   show ?case
   proof (cases "delete x t\<^isub>2")
     case (Some t\<^isub>2')
@@ -507,8 +507,8 @@
   case Tip thus ?case by simp
 next
   case (Node l x d r)
-  have sub: "subtract (Node l x d r) t\<^isub>2 = Some t".
-  have dist_t2: "all_distinct t\<^isub>2".
+  have sub: "subtract (Node l x d r) t\<^isub>2 = Some t" by fact
+  have dist_t2: "all_distinct t\<^isub>2" by fact
   show ?case
   proof (cases "delete x t\<^isub>2")
     case (Some t\<^isub>2')