src/HOL/Induct/ROOT.ML
author berghofe
Wed, 11 Jul 2007 11:14:51 +0200
changeset 23746 a455e69c31cc
parent 17598 7540ccd2b445
child 24104 719fbe4fb77f
permissions -rw-r--r--
Adapted to new inductive definition package.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
17598
wenzelm
parents: 15172
diff changeset
     1
wenzelm
parents: 15172
diff changeset
     2
(* $Id$ *)
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     3
11046
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 10876
diff changeset
     4
time_use_thy "Mutil";
14527
bc9e5587d05a IsaMakefile
paulson
parents: 14505
diff changeset
     5
time_use_thy "QuoDataType";
15172
73069e033a0b new example of a quotiented nested data type
paulson
parents: 14527
diff changeset
     6
time_use_thy "QuoNestedDataType";
11046
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 10876
diff changeset
     7
time_use_thy "Term";
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 10876
diff changeset
     8
time_use_thy "ABexp";
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 10876
diff changeset
     9
time_use_thy "Tree";
11641
0c248bed5225 added Ordinals example;
wenzelm
parents: 11058
diff changeset
    10
time_use_thy "Ordinals";
10876
e12892e4666a added Sigma_Algebra;
wenzelm
parents: 10566
diff changeset
    11
time_use_thy "Sigma_Algebra";
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    12
time_use_thy "Comb";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    13
time_use_thy "PropLog";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    14
time_use_thy "SList";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    15
time_use_thy "LFilter";
23746
a455e69c31cc Adapted to new inductive definition package.
berghofe
parents: 17598
diff changeset
    16
time_use_thy "Com";