src/HOL/plain.ML
author wenzelm
Sat, 18 Jun 2011 18:17:08 +0200
changeset 43445 270bbbcda059
parent 37694 19e8b730ddeb
permissions -rw-r--r--
hardwired abbreviations for standard control symbols;


(* side-entry for HOL-Plain *)

use_thys ["Plain"];