Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
added aT (from axclass.ML);
authorwenzelm
Mon, 10 Apr 2006 00:33:53 +0200
changeset 19394 9f69613362c1
parent 19393 78d6b7a01b12
child 19395 edf92521e8d3
added aT (from axclass.ML); non-pervasive itselfT, a_itselfT;
src/Pure/term.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/term.ML	Mon Apr 10 00:33:52 2006 +0200
+++ b/src/Pure/term.ML	Mon Apr 10 00:33:53 2006 +0200
@@ -84,8 +84,6 @@
   structure Vartab: TABLE
   structure Typtab: TABLE
   structure Termtab: TABLE
-  val itselfT: typ -> typ
-  val a_itselfT: typ
   val propT: typ
   val implies: term
   val all: typ -> term
@@ -162,6 +160,9 @@
 signature TERM =
 sig
   include BASIC_TERM
+  val aT: sort -> typ
+  val itselfT: typ -> typ
+  val a_itselfT: typ
   val argument_type_of: term -> typ
   val add_tvarsT: typ -> (indexname * sort) list -> (indexname * sort) list
   val add_tvars: term -> (indexname * sort) list -> (indexname * sort) list
@@ -695,6 +696,8 @@
 
 (** Connectives of higher order logic **)
 
+fun aT S = TFree ("'a", S);
+
 fun itselfT ty = Type ("itself", [ty]);
 val a_itselfT = itselfT (TFree ("'a", []));
isabelle