author | haftmann |
Tue, 19 May 2009 16:54:55 +0200 | |
changeset 31205 | 98370b26c2ce |
parent 28827 | b3ce1912ac25 |
child 33615 | 261abc2e3155 |
permissions | -rw-r--r-- |
17598 | 1 |
|
2 |
(* $Id$ *) |
|
3120
c58423c20740
New directory to contain examples of (co)inductive definitions
paulson
parents:
diff
changeset
|
3 |
|
28385 | 4 |
setmp_noncritical quick_and_dirty true |
24607 | 5 |
use_thy "Common_Patterns"; |
6 |
||
28827
b3ce1912ac25
removed Induct/Mutil.thy -- the file has been moved to AFP;
wenzelm
parents:
28385
diff
changeset
|
7 |
use_thys ["QuoDataType", "QuoNestedDataType", "Term", |
24104 | 8 |
"ABexp", "Tree", "Ordinals", "Sigma_Algebra", "Comb", "PropLog", |
9 |
"SList", "LFilter", "Com"]; |