added caveat; a real solution would be difficult
authoroheimb
Tue Sep 08 17:07:39 1998 +0200 (1998-09-08)
changeset 5437f68b9d225942
parent 5436 cff7d1e98376
child 5438 c89ee3a46a74
added caveat; a real solution would be difficult
src/Provers/splitter.ML
     1.1 --- a/src/Provers/splitter.ML	Tue Sep 08 17:03:21 1998 +0200
     1.2 +++ b/src/Provers/splitter.ML	Tue Sep 08 17:07:39 1998 +0200
     1.3 @@ -339,6 +339,7 @@
     1.4  	      |   first_prem_is_disj (Const("all",_)$Abs(_,_,t)) = 
     1.5  					first_prem_is_disj t
     1.6  	      |   first_prem_is_disj _ = false;
     1.7 +      (* does not work properly if the split variable is bound by a quantfier *)
     1.8  	      fun flat_prems_tac i = SUBGOAL (fn (t,i) => 
     1.9  			   (if first_prem_is_disj t
    1.10  			    then EVERY[etac Data.disjE i,rotate_tac ~1 i,