# HG changeset patch
# User paulson
# Date 982327041 -3600
# Node ID 950ede59c05a8ca259ad91c57776db070ac3d43f
# Parent  32d002362005d63728c24ca68da14a39f339fbe5
Blast bug fix made old proof too slow

diff -r 32d002362005 -r 950ede59c05a src/HOL/Library/Permutation.thy
--- a/src/HOL/Library/Permutation.thy	Fri Feb 16 13:29:07 2001 +0100
+++ b/src/HOL/Library/Permutation.thy	Fri Feb 16 13:37:21 2001 +0100
@@ -23,11 +23,11 @@
   "x <~~> y" == "(x, y) \<in> perm"
 
 inductive perm
-  intros [intro]
-    Nil: "[] <~~> []"
-    swap: "y # x # l <~~> x # y # l"
-    Cons: "xs <~~> ys ==> z # xs <~~> z # ys"
-    trans: "xs <~~> ys ==> ys <~~> zs ==> xs <~~> zs"
+  intros
+    Nil  [intro!]: "[] <~~> []"
+    swap [intro!]: "y # x # l <~~> x # y # l"
+    Cons [intro!]: "xs <~~> ys ==> z # xs <~~> z # ys"
+    trans [intro]: "xs <~~> ys ==> ys <~~> zs ==> xs <~~> zs"
 
 lemma perm_refl [iff]: "l <~~> l"
   apply (induct l)
@@ -101,7 +101,7 @@
 lemma perm_rev: "rev xs <~~> xs"
   apply (induct xs)
    apply simp_all
-  apply (blast intro: perm_sym perm_append_single)
+  apply (blast intro!: perm_append_single intro: perm_sym)
   done
 
 lemma perm_append1: "xs <~~> ys ==> l @ xs <~~> l @ ys"