src/HOL/Induct/ROOT.ML
author wenzelm
Mon, 01 Oct 2001 11:56:40 +0200
changeset 11641 0c248bed5225
parent 11058 b3e7863a5060
child 13075 d3e1d554cd6d
permissions -rw-r--r--
added Ordinals example;
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";
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 10876
diff changeset
     3
time_use_thy "Term";
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 10876
diff changeset
     4
time_use_thy "ABexp";
b5f5942781a0 Induct: converted some theories to new-style format;
wenzelm
parents: 10876
diff changeset
     5
time_use_thy "Tree";
11641
0c248bed5225 added Ordinals example;
wenzelm
parents: 11058
diff changeset
     6
time_use_thy "Ordinals";
10876
e12892e4666a added Sigma_Algebra;
wenzelm
parents: 10566
diff changeset
     7
time_use_thy "Sigma_Algebra";
3120
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     8
time_use_thy "Comb";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
     9
time_use_thy "PropLog";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    10
time_use_thy "SList";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    11
time_use_thy "LFilter";
c58423c20740 New directory to contain examples of (co)inductive definitions
paulson
parents:
diff changeset
    12
time_use_thy "Exp";