reactivate some examples that still appear to work;
authorwenzelm
Thu Feb 13 12:24:28 2014 +0100 (2014-02-13)
changeset 554509eddc17749f7
parent 55449 ce855dc0e523
child 55451 ea1d9408a233
reactivate some examples that still appear to work;
src/HOL/ROOT
     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 +