/src/HOL/Induct/
drwxr-xr-x [up]
drwxr-xr-x document
-rw-r--r-- 2010-03-02 17:36 +0000 2076 ABexp.thy
-rw-r--r-- 2010-03-02 17:36 +0000 9447 Com.thy
-rw-r--r-- 2010-03-02 17:36 +0000 6123 Comb.thy
-rw-r--r-- 2010-03-02 17:36 +0000 8962 Common_Patterns.thy
-rw-r--r-- 2010-03-02 17:36 +0000 1911 Ordinals.thy
-rw-r--r-- 2010-03-02 17:36 +0000 7510 PropLog.thy
-rw-r--r-- 2010-03-02 17:36 +0000 15347 QuoDataType.thy
-rw-r--r-- 2010-03-02 17:36 +0000 15050 QuoNestedDataType.thy
-rw-r--r-- 2010-03-02 17:36 +0000 1329 README.html
-rw-r--r-- 2010-03-02 17:36 +0000 210 ROOT.ML
-rw-r--r-- 2010-03-02 17:36 +0000 12551 SList.thy
-rw-r--r-- 2010-03-02 17:36 +0000 4653 Sexp.thy
-rw-r--r-- 2010-03-02 17:36 +0000 1754 Sigma_Algebra.thy
-rw-r--r-- 2010-03-02 17:36 +0000 1308 Term.thy
-rw-r--r-- 2010-03-02 17:36 +0000 3083 Tree.thy