src/HOL/Lambda/Commutation.thy
changeset 21669 c68717c16013
parent 21404 eb85850d3eb7
child 22270 4ccb7e6be929
     1.1 --- a/src/HOL/Lambda/Commutation.thy	Tue Dec 05 22:14:53 2006 +0100
     1.2 +++ b/src/HOL/Lambda/Commutation.thy	Wed Dec 06 01:12:36 2006 +0100
     1.3 @@ -130,8 +130,9 @@
     1.4    apply (tactic {* safe_tac HOL_cs *})
     1.5     apply (tactic {*
     1.6       blast_tac (HOL_cs addIs
     1.7 -       [Un_upper2 RS rtrancl_mono RS subsetD RS rtrancl_trans,
     1.8 -       rtrancl_converseI, converseI, Un_upper1 RS rtrancl_mono RS subsetD]) 1 *})
     1.9 +       [thm "Un_upper2" RS thm "rtrancl_mono" RS thm "subsetD" RS thm "rtrancl_trans",
    1.10 +        thm "rtrancl_converseI", thm "converseI",
    1.11 +        thm "Un_upper1" RS thm "rtrancl_mono" RS thm "subsetD"]) 1 *})
    1.12    apply (erule rtrancl_induct)
    1.13     apply blast
    1.14    apply (blast del: rtrancl_refl intro: rtrancl_trans)