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 term_of function for product type.
authorberghofe
Tue, 27 May 2003 17:39:43 +0200
changeset 14049 ef1da11a64b9
parent 14048 03a9adec9869
child 14050 826037db30cd
Added term_of function for product type.
src/HOL/Main.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Main.thy	Tue May 27 17:39:17 2003 +0200
+++ b/src/HOL/Main.thy	Tue May 27 17:39:43 2003 +0200
@@ -44,6 +44,7 @@
 
 val term_of_list = HOLogic.mk_list;
 val term_of_int = HOLogic.mk_int;
+fun term_of_id_42 f T g U (x, y) = HOLogic.pair_const T U $ f x $ g y;
 *}
 
 lemma [code]: "((n::nat) < 0) = False" by simp
isabelle