*** empty log message ***
authoroheimb
Wed Apr 03 20:08:27 1996 +0200 (1996-04-03)
changeset 163869c094639823
parent 1637 b8a8ae2e5de1
child 1639 d3484e841d1e
*** empty log message ***
src/HOLCF/domain/theorems.ML
     1.1 --- a/src/HOLCF/domain/theorems.ML	Wed Apr 03 19:27:14 1996 +0200
     1.2 +++ b/src/HOLCF/domain/theorems.ML	Wed Apr 03 20:08:27 1996 +0200
     1.3 @@ -1,4 +1,4 @@
     1.4 -(* theorems.ML
     1.5 + (* theorems.ML
     1.6     Author : David von Oheimb
     1.7     Created: 06-Jun-95
     1.8     Updated: 08-Jun-95 first proof from cterms
     1.9 @@ -39,10 +39,10 @@
    1.10  
    1.11  fun REPEAT_DETERM_UNTIL p tac = 
    1.12  let fun drep st = if p st then Sequence.single st
    1.13 -			  else (case Sequence.pull(tapply(tac,st)) of
    1.14 +			  else (case Sequence.pull(tac st) of
    1.15  		                  None        => Sequence.null
    1.16  				| Some(st',_) => drep st')
    1.17 -in Tactic drep end;
    1.18 +in drep end;
    1.19  val UNTIL_SOLVED = REPEAT_DETERM_UNTIL (has_fewer_prems 1);
    1.20  
    1.21  local val trueI2 = prove_goal HOL.thy"f~=x ==> True"(fn prems=>[rtac TrueI 1])in