src/Pure/Pure.thy
changeset 18836 3a1e4ee72075
parent 18710 527aa560a9e0
child 19048 2b875dd5eb4c
     1.1 --- a/src/Pure/Pure.thy	Sun Jan 29 19:23:42 2006 +0100
     1.2 +++ b/src/Pure/Pure.thy	Sun Jan 29 19:23:43 2006 +0100
     1.3 @@ -73,7 +73,8 @@
     1.4  lemma imp_conjunction [unfolded prop_def]:
     1.5    includes meta_conjunction_syntax
     1.6    shows "(PROP A ==> PROP prop (PROP B && PROP C)) == (PROP A ==> PROP B) && (PROP A ==> PROP C)"
     1.7 -proof (unfold prop_def, rule)
     1.8 +  unfolding prop_def
     1.9 +proof
    1.10    assume conj: "PROP A ==> PROP B && PROP C"
    1.11    fix X assume r: "(PROP A ==> PROP B) ==> (PROP A ==> PROP C) ==> PROP X"
    1.12    show "PROP X"
    1.13 @@ -121,6 +122,6 @@
    1.14  lemma conjunction_assoc:
    1.15    includes meta_conjunction_syntax
    1.16    shows "((PROP A && PROP B) && PROP C) == (PROP A && (PROP B && PROP C))"
    1.17 -  by (rule equal_intr_rule) (unfold imp_conjunction conjunction_imp)
    1.18 +  unfolding conjunction_imp .
    1.19  
    1.20  end