Blast bug fix made old proof too slow
authorpaulson
Fri Feb 16 13:37:21 2001 +0100 (2001-02-16)
changeset 11153950ede59c05a
parent 11152 32d002362005
child 11154 042015819774
Blast bug fix made old proof too slow
src/HOL/Library/Permutation.thy
     1.1 --- a/src/HOL/Library/Permutation.thy	Fri Feb 16 13:29:07 2001 +0100
     1.2 +++ b/src/HOL/Library/Permutation.thy	Fri Feb 16 13:37:21 2001 +0100
     1.3 @@ -23,11 +23,11 @@
     1.4    "x <~~> y" == "(x, y) \<in> perm"
     1.5  
     1.6  inductive perm
     1.7 -  intros [intro]
     1.8 -    Nil: "[] <~~> []"
     1.9 -    swap: "y # x # l <~~> x # y # l"
    1.10 -    Cons: "xs <~~> ys ==> z # xs <~~> z # ys"
    1.11 -    trans: "xs <~~> ys ==> ys <~~> zs ==> xs <~~> zs"
    1.12 +  intros
    1.13 +    Nil  [intro!]: "[] <~~> []"
    1.14 +    swap [intro!]: "y # x # l <~~> x # y # l"
    1.15 +    Cons [intro!]: "xs <~~> ys ==> z # xs <~~> z # ys"
    1.16 +    trans [intro]: "xs <~~> ys ==> ys <~~> zs ==> xs <~~> zs"
    1.17  
    1.18  lemma perm_refl [iff]: "l <~~> l"
    1.19    apply (induct l)
    1.20 @@ -101,7 +101,7 @@
    1.21  lemma perm_rev: "rev xs <~~> xs"
    1.22    apply (induct xs)
    1.23     apply simp_all
    1.24 -  apply (blast intro: perm_sym perm_append_single)
    1.25 +  apply (blast intro!: perm_append_single intro: perm_sym)
    1.26    done
    1.27  
    1.28  lemma perm_append1: "xs <~~> ys ==> l @ xs <~~> l @ ys"