src/HOL/ROOT
changeset 55450 9eddc17749f7
parent 55447 aa41ecbdc205
child 55596 928b9f677165
     1.1 --- a/src/HOL/ROOT	Thu Feb 13 12:14:47 2014 +0100
     1.2 +++ b/src/HOL/ROOT	Thu Feb 13 12:24:28 2014 +0100
     1.3 @@ -917,19 +917,19 @@
     1.4      (* FIXME
     1.5      Predicate_Compile_Quickcheck_Examples  -- should be added again soon (since 21-Oct-2010) *)
     1.6      Specialisation_Examples
     1.7 -    (* FIXME since 21-Jul-2011
     1.8 -    Hotel_Example_Small_Generator
     1.9      IMP_1
    1.10      IMP_2
    1.11 +    (* FIXME since 21-Jul-2011
    1.12 +    Hotel_Example_Small_Generator
    1.13      IMP_3
    1.14      IMP_4 *)
    1.15 -  theories [condition = "ISABELLE_SWIPL"]  (* FIXME: *or* ISABELLE_YAP (??) *)
    1.16 +  theories [condition = "ISABELLE_SWIPL"]
    1.17      Code_Prolog_Examples
    1.18      Context_Free_Grammar_Example
    1.19      Hotel_Example_Prolog
    1.20      Lambda_Example
    1.21      List_Examples
    1.22 -  theories [condition = "ISABELLE_SWIPL", quick_and_dirty]  (* FIXME: *or* ISABELLE_YAP (??) *)
    1.23 +  theories [condition = "ISABELLE_SWIPL", quick_and_dirty]
    1.24      Reg_Exp_Example
    1.25  
    1.26  session HOLCF (main) in HOLCF = HOL +