doc-src/Classes/Thy/ROOT.ML
author bulwahn
Wed, 31 Mar 2010 16:44:41 +0200
changeset 36057 ca6610908ae9
parent 30226 2f4684e2ea95
child 42637 381fdcab0f36
permissions -rw-r--r--
adding MREC induction rule in Imperative HOL


(* $Id$ *)

no_document use_thy "Setup";

use_thy "Classes";