src/HOL/Main.thy
changeset 14049 ef1da11a64b9
parent 13755 a9bb54a3cfb7
child 14102 8af7334af4b3
     1.1 --- a/src/HOL/Main.thy	Tue May 27 17:39:17 2003 +0200
     1.2 +++ b/src/HOL/Main.thy	Tue May 27 17:39:43 2003 +0200
     1.3 @@ -44,6 +44,7 @@
     1.4  
     1.5  val term_of_list = HOLogic.mk_list;
     1.6  val term_of_int = HOLogic.mk_int;
     1.7 +fun term_of_id_42 f T g U (x, y) = HOLogic.pair_const T U $ f x $ g y;
     1.8  *}
     1.9  
    1.10  lemma [code]: "((n::nat) < 0) = False" by simp