author | wenzelm |
Thu, 27 Jul 2000 18:23:12 +0200 | |
changeset 9450 | c97dba47e504 |
parent 9000 | c20d58286a51 |
child 9951 | 5610c4acb48d |
permissions | -rw-r--r-- |
(* Title: HOL/Induct/ROOT.ML Examples of Inductive and Coinductive Definitions. *) time_use_thy "Perm"; time_use_thy "Comb"; time_use_thy "Mutil"; time_use_thy "Acc"; time_use_thy "MultisetOrder"; time_use_thy "PropLog"; time_use_thy "SList"; time_use_thy "LFilter"; time_use_thy "Term"; time_use_thy "ABexp"; time_use_thy "Exp"; time_use_thy "Tree";