Re: [Hol-developers] [Hol-checkins] CVS: hol98/src/num/theories arithmeticScript.sml,1.42,1.43

[<sl...@cs...>]

Quoting Michael Norrish <Mic...@ni...>:

 > 
> Also, you can always write your own:
> 
>   fun q by tac = Q.SUBGOAL_THEN q STRIP_ASSUME_TAC THEN1 tac
> 
> though this is not quite the same as the "by" in SingleStep because it
> insists that tac solve the goal completely.  (Actually this strikes me
> as an improvement.)

I've found "q by ALL_TAC" is a nice way to get started on a multi-step
proof of q, and this style of use wouldn't be allowed under the 
suggested improvement.

Konrad.