Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2004-07-08 19:53:08 -0700 (Thu, 08 Jul 2004)
Revision: 6049
Log message:

      Aleksey Nogin wrote:
      
      > You defined the ITT's is_bterm to be a boolean. Wouldn't it be
      > better to define it as a prop (if_bterm{'bt; true})?
      > The thing is only well-formed when it is true, so it has
      > a certain "propositionality" to it. And this way, of course,
      >there will be no need to assert it all the time.
      
      I agree.
      

Changes	Path
+2 -2	metaprl/theories/itt/itt_reflection_test.ml