src/HOL/Induct/ROOT.ML
author haftmann
Fri, 17 Jun 2005 16:12:49 +0200
changeset 16417 9bc16273c2d4
parent 15172 73069e033a0b
child 17598 7540ccd2b445
permissions -rw-r--r--
migrated theory headers to new format
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     1
11046
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 10876
diff changeset
     2
time_use_thy "Mutil";
14527
bc9e5587d05a IsaMakefile
paulson
parents: 14505
diff changeset
     3
time_use_thy "QuoDataType";
15172
73069e033a0b new example of a quotiented nested data type
paulson
parents: 14527
diff changeset
     4
time_use_thy "QuoNestedDataType";
11046
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 10876
diff changeset
     5
time_use_thy "Term";
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 10876
diff changeset
     6
time_use_thy "ABexp";
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 10876
diff changeset
     7
time_use_thy "Tree";
11641
0c248bed5225 added Ordinals example;
wenzelm
parents: 11058
diff changeset
     8
time_use_thy "Ordinals";
10876
e12892e4666a added Sigma_Algebra;
wenzelm
parents: 10566
diff changeset
     9
time_use_thy "Sigma_Algebra";
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    10
time_use_thy "Comb";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    11
time_use_thy "PropLog";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    12
time_use_thy "SList";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    13
time_use_thy "LFilter";
14288
d149e3cbdb39 Moving some theorems from Real/RealArith0.ML
paulson
parents: 13075
diff changeset
    14