Measure functions can now be declared via special rules, allowing for a
prolog-style generation of measure functions for a specific type.
(* Title: HOL/Main.thy
ID: $Id$
*)
header {* Main HOL *}
theory Main
imports Map
begin
ML {* val HOL_proofs = ! Proofterm.proofs *}
ML {* path_add "~~/src/HOL/Library" *}
end