src/HOL/plain.ML
author haftmann
Sun, 19 Feb 2012 15:30:35 +0100
changeset 46553 50a7e97fe653
parent 37694 19e8b730ddeb
permissions -rw-r--r--
distributed lattice properties of predicates to places of instantiation


(* side-entry for HOL-Plain *)

use_thys ["Plain"];