src/HOL/base.ML
author wenzelm
Fri, 06 Apr 2012 12:02:24 +0200
changeset 47347 af937661e4a1
parent 37694 19e8b730ddeb
permissions -rw-r--r--
stop node execution at first unassigned exec;


(* side-entry for HOL-Base *)

use_thys ["HOL"];