| changeset 20593 | 5af400cc64d5 |
| parent 17604 | 5f30179fbf44 |
| child 20837 | 099877d83d2b |
--- a/src/HOL/Extraction/Pigeonhole.thy Tue Sep 19 15:21:51 2006 +0200 +++ b/src/HOL/Extraction/Pigeonhole.thy Tue Sep 19 15:21:52 2006 +0200 @@ -285,6 +285,9 @@ consts_code arbitrary :: "nat \<times> nat" ("{* (0::nat, 0::nat) *}") +code_const "arbitrary \<Colon> nat \<times> nat" + (SML "{* (0\<Colon>nat, 0\<Colon>nat) *}") + code_module PH contains test = "\<lambda>n. pigeonhole n (\<lambda>m. m - 1)"