# HG changeset patch
# User wenzelm
# Date 1344247149 -7200
# Node ID c1499b14b48c4de2772cadea8f01332363e5c5a5
# Parent  ebbd70082e657b30c6b521777c3af97a1f694bd0
more precise imitation of old ROOT.ML files;

diff -r ebbd70082e65 -r c1499b14b48c src/HOL/ROOT
--- a/src/HOL/ROOT	Sun Aug 05 23:37:26 2012 +0200
+++ b/src/HOL/ROOT	Mon Aug 06 11:59:09 2012 +0200
@@ -36,7 +36,7 @@
     Code_Char_ord
     Code_Integer
     Efficient_Nat
-    (*"Code_Prolog" FIXME*)
+    (*"Code_Prolog" FIXME cf. 76965c356d2a *)
     Code_Real_Approx_By_Float
     Target_Numeral
   files "document/root.bib" "document/root.tex"
@@ -471,7 +471,8 @@
     Set_Comprehension_Pointfree_Tests
     Parallel_Example
   theories SVC_Oracle
-  theories [condition = SVC_HOME] svc_test
+  theories [condition = SVC_HOME]
+    svc_test
   theories [condition = ZCHAFF_HOME]
     (*requires zChaff (or some other reasonably fast SAT solver)*)
     Sudoku
@@ -739,7 +740,12 @@
 session Quickcheck_Examples = HOL +
   options [timeout = 3600, document = false]
   theories
-    Quickcheck_Examples (* FIXME more *)
+    Quickcheck_Examples
+  (* FIXME
+    Quickcheck_Lattice_Examples
+    Completeness
+    Quickcheck_Interfaces
+    Hotel_Example *)
   theories [condition = ISABELLE_GHC]
     Quickcheck_Narrowing_Examples
 
@@ -748,7 +754,7 @@
     Find_Unused_Assms_Examples
     Needham_Schroeder_No_Attacker_Example
     Needham_Schroeder_Guided_Attacker_Example
-    Needham_Schroeder_Unguided_Attacker_Example (* FIXME more *)
+    Needham_Schroeder_Unguided_Attacker_Example
 
 session Quotient_Examples = HOL +
   description {*
@@ -768,10 +774,26 @@
 
 session Predicate_Compile_Examples = HOL +
   options [document = false]
-  theories  (* FIXME *)
+  theories
     Examples
     Predicate_Compile_Tests
+    (* FIXME
+    Predicate_Compile_Quickcheck_Examples  -- should be added again soon (since 21-Oct-2010) *)
     Specialisation_Examples
+    (* FIXME since 21-Jul-2011
+    Hotel_Example_Small_Generator
+    IMP_1
+    IMP_2
+    IMP_3
+    IMP_4 *)
+  theories [condition = "ISABELLE_SWIPL"]  (* FIXME: *or* ISABELLE_YAP (??) *)
+    Code_Prolog_Examples
+    Context_Free_Grammar_Example
+    Hotel_Example_Prolog
+    Lambda_Example
+    List_Examples
+  theories [condition = "ISABELLE_SWIPL", quick_and_dirty]  (* FIXME: *or* ISABELLE_YAP (??) *)
+    Reg_Exp_Example
 
 session HOLCF! (main) = HOL +
   description {*