src/HOL/plain.ML
author bulwahn
Wed, 10 Oct 2012 10:48:55 +0200
changeset 49768 3ecfba7e731d
parent 37694 19e8b730ddeb
permissions -rw-r--r--
adding necessary syntactic functions in set_comprehension_pointfree simproc as a first step to integrate an improved simproc


(* side-entry for HOL-Plain *)

use_thys ["Plain"];