TFL/usyntax.sml
changeset 8882 9df44a4f1bf7
parent 6498 1ebbe18fe236
child 9373 78a11a353473
equal deleted inserted replaced
8881:0467dd0d66ff 8882:9df44a4f1bf7
   319         in (R,y,x)
   319         in (R,y,x)
   320         end handle _ => raise USYN_ERR{func="dest_relation",
   320         end handle _ => raise USYN_ERR{func="dest_relation",
   321                                   mesg="unexpected term structure"}
   321                                   mesg="unexpected term structure"}
   322    else raise USYN_ERR{func="dest_relation",mesg="not a boolean term"};
   322    else raise USYN_ERR{func="dest_relation",mesg="not a boolean term"};
   323 
   323 
   324 fun is_WFR (Const("wf",_)$_) = true
   324 fun is_WFR (Const("WF.wf",_)$_) = true
   325   | is_WFR _                 = false;
   325   | is_WFR _                 = false;
   326 
   326 
   327 fun ARB ty = mk_select{Bvar=Free("v",ty),
   327 fun ARB ty = mk_select{Bvar=Free("v",ty),
   328                        Body=Const("True",HOLogic.boolT)};
   328                        Body=Const("True",HOLogic.boolT)};
   329 
   329