src/HOL/Real.thy
author immler@in.tum.de
Wed, 03 Jun 2009 16:56:41 +0200
changeset 31409 d8537ba165b5
parent 29197 6d4cb27ed19c
child 32877 6f09346c7c08
permissions -rw-r--r--
split preparing clauses and writing problemfile; included results of count_constants in return-type of prover; optionally pass counted constants to prover; removed unused external_prover from signature

theory Real
imports RComplete RealVector
begin

end