src/HOL/MicroJava/ROOT.ML
author wenzelm
Tue, 21 Jul 2009 01:03:18 +0200
changeset 32091 30e2ffbba718
parent 27680 5a557a5afc48
child 33615 261abc2e3155
permissions -rw-r--r--
proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;

(* $Id$ *)

no_document use_thy "While_Combinator";

use_thy "MicroJava";