Re: [isabelle] Isabelle2016-RC0 - text with cartouches outside theory



Hi,

In HOL/ex/ML.thy, moving the following line before the theory command gives an error message, but why?

text âSee ðâhttp://mathworld.wolfram.com/AckermannFunction.htmlâ.â;

By the way, is there a short expression for the following line used in the Scala console for batch processing?

Build.build(Options.init, select_dirs = List(Path.explode("~/Documents")))

Thanks,

JÃrgen



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