src/HOL/Real.thy
author bulwahn
Tue, 23 Feb 2010 13:36:15 +0100
changeset 35324 c9f428269b38
parent 35090 88cc65ae046e
child 36899 bcd6fce5bf06
permissions -rw-r--r--
adopting mutabelle and quickcheck to return timing information; exporting make_case_combs in datatype package for predicate compiler; adding Spec_Rules declaration for tail recursive functions; improving the predicate compiler and function flattening

theory Real
imports RComplete RealVector
begin

end