src/HOL/ROOT.ML
author wenzelm
Tue, 22 Mar 2011 14:45:48 +0100
changeset 42051 dbdd4790da34
parent 37694 19e8b730ddeb
permissions -rw-r--r--
let syntax: reverted to plain "id", since translations cannot cope with constraints (notably position information);


(* Classical Higher-order Logic *)

use_thys ["Complex_Main"];