fixed assumption proof;
authorwenzelm
Fri Jan 02 11:31:07 2009 +0100 (2009-01-02)
changeset 2930576af2a3c9d28
parent 29304 5c71a6da989d
child 29306 2c764235e041
fixed assumption proof;
src/FOLP/IFOLP.thy
     1.1 --- a/src/FOLP/IFOLP.thy	Fri Jan 02 00:21:59 2009 +0100
     1.2 +++ b/src/FOLP/IFOLP.thy	Fri Jan 02 11:31:07 2009 +0100
     1.3 @@ -339,6 +339,7 @@
     1.4    shows "?a : R"
     1.5    apply (insert assms(1) [unfolded ex1_def])
     1.6    apply (erule exE conjE | assumption | rule assms(1))+
     1.7 +  apply (erule assms(2), assumption)
     1.8    done
     1.9  
    1.10