# HG changeset patch
# User wenzelm
# Date 1343829396 -7200
# Node ID 38793f924c9aa3cf270d8332650d0534ddaa692f
# Parent  bfce940c6f388e9bc57b856e148704a61453e244
added offline test for skip_proofs;

diff -r bfce940c6f38 -r 38793f924c9a src/HOL/ROOT
--- a/src/HOL/ROOT	Wed Aug 01 15:50:50 2012 +0200
+++ b/src/HOL/ROOT	Wed Aug 01 15:56:36 2012 +0200
@@ -341,6 +341,10 @@
     "document/root.bib"
     "document/root.tex"
 
+session "MicroJava-skip_proofs" in MicroJava = HOL +
+  options [condition = ISABELLE_FULL_TEST, document = false, skip_proofs, quick_and_dirty]
+  theories MicroJava
+
 session NanoJava = HOL +
   options [document_graph]
   theories Example