added logicC: class, logicS: sort;
authorwenzelm
Wed May 18 15:20:54 1994 +0200 (1994-05-18)
changeset 375d7ae7ac22d48
parent 374 caf9a9b7f605
child 376 d3d01131470f
added logicC: class, logicS: sort;
added itselfT: typ -> typ, a_itselfT: typ (for axclasses);
src/Pure/term.ML
     1.1 --- a/src/Pure/term.ML	Wed May 18 15:19:25 1994 +0200
     1.2 +++ b/src/Pure/term.ML	Wed May 18 15:20:54 1994 +0200
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title: 	term.ML
     1.5 +(*  Title: 	Pure/term.ML
     1.6      ID:         $Id$
     1.7      Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.8      Copyright   Cambridge University 1992
     1.9 @@ -213,6 +213,12 @@
    1.10  
    1.11  (** Connectives of higher order logic **)
    1.12  
    1.13 +val logicC: class = "logic";
    1.14 +val logicS: sort = [logicC];
    1.15 +
    1.16 +fun itselfT ty = Type ("itself", [ty]);
    1.17 +val a_itselfT = itselfT (TFree ("'a", logicS));
    1.18 +
    1.19  val propT : typ = Type("prop",[]);
    1.20  
    1.21  val implies = Const("==>", propT-->propT-->propT);