Re: [isabelle] Mixed decimals and Real.thy

Here I suggest that you build the logic HOL-Complex and then use as your first line

theory Test imports Complex_Main

Larry Paulson

On 14 Mar 2006, at 18:29, <jdavis27 at> <jdavis27 at> wrote:

The following snippet works as expected in Isabelle2005:

ML "add_path \"$ISABELLE_HOME/src/HOL/Real\"";
theory Test = Main + Real:

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.