src/HOL/ROOT.ML
author blanchet
Sun, 01 May 2011 18:37:24 +0200
changeset 42557 ae0deb39a254
parent 37694 19e8b730ddeb
permissions -rw-r--r--
fixed min-arity computation when "explicit_apply" is specified


(* Classical Higher-order Logic *)

use_thys ["Complex_Main"];