src/HOL/ex/ROOT.ML
changeset 5753 c90b5f7d0c61
parent 5368 7c8d1c7c876d
child 5866 de6a1856c74a
equal deleted inserted replaced
5752:c3df312f34a2 5753:c90b5f7d0c61
     9 HOL_build_completed;    (*Cause examples to fail if HOL did*)
     9 HOL_build_completed;    (*Cause examples to fail if HOL did*)
    10 
    10 
    11 writeln "Root file for HOL examples";
    11 writeln "Root file for HOL examples";
    12 set proof_timing;
    12 set proof_timing;
    13 
    13 
    14 (**Some examples of recursive function definitions: the TFL package**)
    14 (*some examples of recursive function definitions: the TFL package*)
    15 time_use_thy "Recdefs";
    15 time_use_thy "Recdefs";
    16 time_use_thy "Primes";
    16 time_use_thy "Primes";
    17 time_use_thy "Fib";
    17 time_use_thy "Fib";
    18 time_use_thy "Primrec";
    18 time_use_thy "Primrec";
    19 
    19 
    33 time_use_thy "MT";
    33 time_use_thy "MT";
    34 
    34 
    35 time_use_thy "StringEx";
    35 time_use_thy "StringEx";
    36 time_use_thy "BinEx";
    36 time_use_thy "BinEx";
    37 
    37 
    38 (*Monoids and Groups as predicates over record schemes*)
    38 (*basic use of extensible records*)
    39 time_use_thy "MonoidGroup";
    39 time_use_thy "MonoidGroup";
       
    40 time_use_thy "Points";
    40 
    41 
    41 (*Groups via locales*)
    42 (*groups via locales*)
    42 time_use_thy "PiSets";
    43 time_use_thy "PiSets";
    43 time_use_thy "LocaleGroup";
    44 time_use_thy "LocaleGroup";
    44 
    45 
    45 (*Expressions with quote / antiquote*)
    46 (*expressions with quote / antiquote syntax*)
    46 time_use_thy "Antiquote";
    47 time_use_thy "Antiquote";
    47 
    48 
    48 
    49 
    49 writeln "END: Root file for HOL examples";
    50 writeln "END: Root file for HOL examples";