src/HOL/base.ML
author wenzelm
Sat, 30 Apr 2011 23:20:50 +0200
changeset 42508 e21362bf1d93
parent 37694 19e8b730ddeb
permissions -rw-r--r--
allow nested @{antiq} (nonterminal) and @@{antiq} terminal;


(* side-entry for HOL-Base *)

use_thys ["HOL"];