src/HOL/ex/ROOT.ML
changeset 24528 e8197c9f1b5c
parent 24478 fb5e3fcfc10c
child 24530 1bac25879117
equal deleted inserted replaced
24527:888d56a8d9d3 24528:e8197c9f1b5c
     2     ID:         $Id$
     2     ID:         $Id$
     3 
     3 
     4 Miscellaneous examples for Higher-Order Logic.
     4 Miscellaneous examples for Higher-Order Logic.
     5 *)
     5 *)
     6 
     6 
     7 no_document use_thys  [
     7 no_document use_thys [
     8   "Parity",
     8   "Parity",
     9   "GCD"
     9   "GCD"
    10 ];
    10 ];
    11 
    11 
    12 use_thys [
    12 use_thys [