Mercurial Mercurial > repos > isabelle / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Extraction/Pigeonhole.thy
changeset 21545 54cc492d80a9
parent 21404 eb85850d3eb7
child 22507 3572bc633d9a
equal deleted inserted replaced
21544:a9ceeb182cfc 21545:54cc492d80a9 
   314 definition
 
   314 definition
 
   315   "test n = pigeonhole n (\<lambda>m. m - 1)"
 
   315   "test n = pigeonhole n (\<lambda>m. m - 1)"
 
   316 definition
 
   316 definition
 
   317   "test' n = pigeonhole_slow n (\<lambda>m. m - 1)"
 
   317   "test' n = pigeonhole_slow n (\<lambda>m. m - 1)"
 
   318 
   318 
   319 code_gen test test' "op !" (SML *)
 
   319 code_gen test test' "op !" (SML #)
 
   320 
   320 
   321 ML "timeit (fn () => ROOT.Pigeonhole.test 10)"
 
   321 ML "timeit (fn () => ROOT.Pigeonhole.test 10)"
 
   322 ML "timeit (fn () => ROOT.Pigeonhole.test' 10)"
 
   322 ML "timeit (fn () => ROOT.Pigeonhole.test' 10)"
 
   323 ML "timeit (fn () => ROOT.Pigeonhole.test 20)"
 
   323 ML "timeit (fn () => ROOT.Pigeonhole.test 20)"
 
   324 ML "timeit (fn () => ROOT.Pigeonhole.test' 20)"
 
   324 ML "timeit (fn () => ROOT.Pigeonhole.test' 20)"
isabelle