src/HOL/Library/Permutation.thy
changeset 11153 950ede59c05a
parent 11054 a5404c70982f
child 14706 71590b7733b7
--- 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"