/src/HOL/
drwxr-xr-x [up]
drwxr-xr-x Algebra
drwxr-xr-x Auth
drwxr-xr-x AxClasses
drwxr-xr-x BCV
drwxr-xr-x Hoare
drwxr-xr-x IMP
drwxr-xr-x IOA
drwxr-xr-x Induct
drwxr-xr-x Integ
drwxr-xr-x Isar_examples
drwxr-xr-x Lambda
drwxr-xr-x Lex
drwxr-xr-x MicroJava
drwxr-xr-x MiniML
drwxr-xr-x Modelcheck
drwxr-xr-x Quot
drwxr-xr-x Real
drwxr-xr-x Subst
drwxr-xr-x TLA
drwxr-xr-x Tools
drwxr-xr-x UNITY
drwxr-xr-x W0
drwxr-xr-x ex
-rw-r--r-- 1999-11-11 12:24 +0100 32424 Arith.ML
-rw-r--r-- 1999-11-11 12:24 +0100 611 Arith.thy
-rw-r--r-- 1999-11-11 12:24 +0100 1800 Calculation.thy
-rw-r--r-- 1999-11-11 12:24 +0100 957 Datatype.ML
-rw-r--r-- 1999-11-11 12:24 +0100 437 Datatype.thy
-rw-r--r-- 1999-11-11 12:24 +0100 15426 Divides.ML
-rw-r--r-- 1999-11-11 12:24 +0100 1052 Divides.thy
-rw-r--r-- 1999-11-11 12:24 +0100 26210 Finite.ML
-rw-r--r-- 1999-11-11 12:24 +0100 1802 Finite.thy
-rw-r--r-- 1999-11-11 12:24 +0100 13342 Fun.ML
-rw-r--r-- 1999-11-11 12:24 +0100 2638 Fun.thy
-rw-r--r-- 1999-11-11 12:24 +0100 4248 Gfp.ML
-rw-r--r-- 1999-11-11 12:24 +0100 362 Gfp.thy
-rw-r--r-- 1999-11-11 12:24 +0100 678 HOL.ML
-rw-r--r-- 1999-11-11 12:24 +0100 6353 HOL.thy
-rw-r--r-- 1999-11-11 12:24 +0100 13516 HOL_lemmas.ML
-rw-r--r-- 1999-11-11 12:24 +0100 583 Inductive.thy
-rw-r--r-- 1999-11-11 12:24 +0100 18748 IsaMakefile
-rw-r--r-- 1999-11-11 12:24 +0100 2420 Lfp.ML
-rw-r--r-- 1999-11-11 12:24 +0100 352 Lfp.thy
-rw-r--r-- 1999-11-11 12:24 +0100 33666 List.ML
-rw-r--r-- 1999-11-11 12:24 +0100 5849 List.thy
-rw-r--r-- 1999-11-11 12:24 +0100 135 Main.thy
-rw-r--r-- 1999-11-11 12:24 +0100 3698 Map.ML
-rw-r--r-- 1999-11-11 12:24 +0100 1671 Map.thy
-rw-r--r-- 1999-11-11 12:24 +0100 2867 Nat.ML
-rw-r--r-- 1999-11-11 12:24 +0100 473 Nat.thy
-rw-r--r-- 1999-11-11 12:24 +0100 14793 NatDef.ML
-rw-r--r-- 1999-11-11 12:24 +0100 1231 NatDef.thy
-rw-r--r-- 1999-11-11 12:24 +0100 499 Numeral.thy
-rw-r--r-- 1999-11-11 12:24 +0100 1914 Option.ML
-rw-r--r-- 1999-11-11 12:24 +0100 517 Option.thy
-rw-r--r-- 1999-11-11 12:24 +0100 6481 Ord.ML
-rw-r--r-- 1999-11-11 12:24 +0100 2591 Ord.thy
-rw-r--r-- 1999-11-11 12:24 +0100 3184 Power.ML
-rw-r--r-- 1999-11-11 12:24 +0100 600 Power.thy
-rw-r--r-- 1999-11-11 12:24 +0100 15910 Prod.ML
-rw-r--r-- 1999-11-11 12:24 +0100 2804 Prod.thy
-rw-r--r-- 1999-11-11 12:24 +0100 2703 README.html
-rw-r--r-- 1999-11-11 12:24 +0100 977 ROOT.ML
-rw-r--r-- 1999-11-11 12:24 +0100 740 Recdef.thy
-rw-r--r-- 1999-11-11 12:24 +0100 1845 Record.thy
-rw-r--r-- 1999-11-11 12:24 +0100 3136 RelPow.ML
-rw-r--r-- 1999-11-11 12:24 +0100 317 RelPow.thy
-rw-r--r-- 1999-11-11 12:24 +0100 9646 Relation.ML
-rw-r--r-- 1999-11-11 12:24 +0100 1769 Relation.thy
-rw-r--r-- 1999-11-11 12:24 +0100 4720 SVC_Oracle.ML
-rw-r--r-- 1999-11-11 12:24 +0100 466 SVC_Oracle.thy
-rw-r--r-- 1999-11-11 12:24 +0100 18943 Set.ML
-rw-r--r-- 1999-11-11 12:24 +0100 7493 Set.thy
-rw-r--r-- 1999-11-11 12:24 +0100 3922 Sexp.ML
-rw-r--r-- 1999-11-11 12:24 +0100 1122 Sexp.thy
-rw-r--r-- 1999-11-11 12:24 +0100 2312 String.thy
-rw-r--r-- 1999-11-11 12:24 +0100 4477 Sum.ML
-rw-r--r-- 1999-11-11 12:24 +0100 1174 Sum.thy
-rw-r--r-- 1999-11-11 12:24 +0100 11629 Trancl.ML
-rw-r--r-- 1999-11-11 12:24 +0100 774 Trancl.thy
-rw-r--r-- 1999-11-11 12:24 +0100 15792 Univ.ML
-rw-r--r-- 1999-11-11 12:24 +0100 3509 Univ.thy
-rw-r--r-- 1999-11-11 12:24 +0100 2163 Vimage.ML
-rw-r--r-- 1999-11-11 12:24 +0100 355 Vimage.thy
-rw-r--r-- 1999-11-11 12:24 +0100 12138 WF.ML
-rw-r--r-- 1999-11-11 12:24 +0100 951 WF.thy
-rw-r--r-- 1999-11-11 12:24 +0100 6933 WF_Rel.ML
-rw-r--r-- 1999-11-11 12:24 +0100 1074 WF_Rel.thy
-rw-r--r-- 1999-11-11 12:24 +0100 1042 blastdata.ML
-rw-r--r-- 1999-11-11 12:24 +0100 1559 cladata.ML
-rw-r--r-- 1999-11-11 12:24 +0100 21615 equalities.ML
-rw-r--r-- 1999-11-11 12:24 +0100 258 equalities.thy
-rw-r--r-- 1999-11-11 12:24 +0100 6648 hologic.ML
-rw-r--r-- 1999-11-11 12:24 +0100 3148 mono.ML
-rw-r--r-- 1999-11-11 12:24 +0100 196 mono.thy
-rw-r--r-- 1999-11-11 12:24 +0100 18986 simpdata.ML
-rw-r--r-- 1999-11-11 12:24 +0100 2556 subset.ML
-rw-r--r-- 1999-11-11 12:24 +0100 271 subset.thy
-rw-r--r-- 1999-11-11 12:24 +0100 9504 thy_syntax.ML