src/HOL/ROOT
changeset 50138 ca989d793b34
parent 50050 fac2b27893ff
child 50149 aaf276a28551
equal deleted inserted replaced
50137:0226d408058b 50138:ca989d793b34
    47     Code_Integer
    47     Code_Integer
    48     Efficient_Nat
    48     Efficient_Nat
    49     (* Code_Prolog  FIXME cf. 76965c356d2a *)
    49     (* Code_Prolog  FIXME cf. 76965c356d2a *)
    50     Code_Real_Approx_By_Float
    50     Code_Real_Approx_By_Float
    51     Code_Target_Numeral
    51     Code_Target_Numeral
       
    52     IArray
    52     Refute
    53     Refute
    53   theories [condition = ISABELLE_FULL_TEST]
    54   theories [condition = ISABELLE_FULL_TEST]
    54     Sum_of_Squares_Remote
    55     Sum_of_Squares_Remote
    55   files "document/root.bib" "document/root.tex"
    56   files "document/root.bib" "document/root.tex"
    56 
    57 
   482     Simproc_Tests
   483     Simproc_Tests
   483     Executable_Relation
   484     Executable_Relation
   484     FinFunPred
   485     FinFunPred
   485     Set_Comprehension_Pointfree_Tests
   486     Set_Comprehension_Pointfree_Tests
   486     Parallel_Example
   487     Parallel_Example
       
   488     IArray_Examples
   487   theories SVC_Oracle
   489   theories SVC_Oracle
   488   theories [condition = SVC_HOME]
   490   theories [condition = SVC_HOME]
   489     svc_test
   491     svc_test
   490   theories [condition = ZCHAFF_HOME]
   492   theories [condition = ZCHAFF_HOME]
   491     (*requires zChaff (or some other reasonably fast SAT solver)*)
   493     (*requires zChaff (or some other reasonably fast SAT solver)*)