src/HOL/ROOT.ML
author wenzelm
Thu, 02 Sep 2010 23:45:37 +0200
changeset 39045 30f3d9daaa3a
parent 37694 19e8b730ddeb
permissions -rw-r--r--
inner parsing: refrain from too many nested position reports to achieve more precise error feedback in the source;


(* Classical Higher-order Logic *)

use_thys ["Complex_Main"];