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 uiuc.edu> <jdavis27 at uiuc.edu> 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.