src/HOL/plain.ML
author krauss
Mon, 23 May 2011 10:58:21 +0200
changeset 42949 618adb3584e5
parent 37694 19e8b730ddeb
permissions -rw-r--r--
separate initializations for different modes of partial_function -- generation of induction rules will be non-uniform


(* side-entry for HOL-Plain *)

use_thys ["Plain"];