src/HOL/base.ML
author huffman
Tue, 23 Aug 2011 14:11:02 -0700
changeset 44457 d366fa5551ef
parent 37694 19e8b730ddeb
permissions -rw-r--r--
declare euclidean_simps [simp] at the point they are proved; avoid duplicate rule warnings;


(* side-entry for HOL-Base *)

use_thys ["HOL"];