src/HOL/ex/ROOT.ML
author chaieb
Wed Sep 14 17:25:52 2005 +0200 (2005-09-14)
changeset 17378 105519771c67
parent 15871 e524119dbf19
child 17413 89ccb3799428
permissions -rw-r--r--
The oracle for Presburger has been changer: It is automatically generated form a verified formaliztion of Cooper's Algorithm ex/Reflected_Presburger.thy
comm_ring : a reflected Method for proving equalities in a commutative ring
     1 (*  Title:      HOL/ex/ROOT.ML
     2     ID:         $Id$
     3 
     4 Miscellaneous examples for Higher-Order Logic.
     5 *)
     6 
     7 time_use_thy "Higher_Order_Logic";
     8 
     9 time_use_thy "Recdefs";
    10 time_use_thy "InductiveInvariant_examples";
    11 time_use_thy "Primrec";
    12 time_use_thy "Locales";
    13 time_use_thy "Records";
    14 time_use_thy "MonoidGroup";
    15 time_use_thy "StringEx";
    16 time_use_thy "BinEx";
    17 setmp proofs 2 time_use_thy "Hilbert_Classical";
    18 time_use_thy "Antiquote";
    19 time_use_thy "Multiquote";
    20 time_use_thy "Tuple";
    21 
    22 time_use_thy "NatSum";
    23 time_use_thy "Intuitionistic";
    24 time_use_thy "Classical";
    25 time_use_thy "CTL";
    26 time_use_thy "mesontest2";
    27 time_use_thy "PresburgerEx";
    28 time_use_thy "Reflected_Presburger";
    29 time_use_thy "BT";
    30 time_use_thy "InSort";
    31 time_use_thy "Qsort";
    32 time_use_thy "MergeSort";
    33 time_use_thy "Puzzle";
    34 
    35 
    36 time_use_thy "Lagrange";
    37 time_use_thy "Commutative_RingEx";
    38 time_use_thy "Commutative_Ring_Complete";
    39 
    40 time_use_thy "set";
    41 time_use_thy "MT";
    42 
    43 no_document use_thy "FuncSet";
    44 time_use_thy "Tarski";
    45 
    46 time_use_thy "SVC_Oracle";
    47 if_svc_enabled time_use_thy "svc_test";
    48 
    49 time_use_thy "Refute_Examples";
    50 time_use_thy "Quickcheck_Examples";
    51 
    52 no_document use_thy "Word";
    53 time_use_thy "Adder";
    54