--- 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 {*