src/Pure/term.ML
changeset 375 d7ae7ac22d48
parent 61 f8c1922b78e3
child 728 9a973c3ba350
     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);