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 range-type for completeness
authorpaulson
Mon, 22 Dec 1997 12:22:06 +0100
changeset 4464 7a8150506746
parent 4463 76769b48bd88
child 4465 7ba65fe66c73
Added range-type for completeness
src/Pure/term.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/term.ML	Mon Dec 22 12:21:37 1997 +0100
+++ b/src/Pure/term.ML	Mon Dec 22 12:22:06 1997 +0100
@@ -254,7 +254,8 @@
   | dest_Var t = raise TERM("dest_Var", [t]);
 
 
-fun domain_type (Type("fun", [T,_])) = T;
+fun domain_type (Type("fun", [T,_])) = T
+and range_type  (Type("fun", [_,T])) = T;
 
 (* maps  [T1,...,Tn]--->T  to the list  [T1,T2,...,Tn]*)
 fun binder_types (Type("fun",[S,T])) = S :: binder_types T
isabelle