/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 IMPP
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-- 2000-02-21 13:57 +0100 32563 Arith.ML
-rw-r--r-- 2000-02-21 13:57 +0100 611 Arith.thy
-rw-r--r-- 2000-02-21 13:57 +0100 1825 Calculation.thy
-rw-r--r-- 2000-02-21 13:57 +0100 957 Datatype.ML
-rw-r--r-- 2000-02-21 13:57 +0100 437 Datatype.thy
-rw-r--r-- 2000-02-21 13:57 +0100 15426 Divides.ML
-rw-r--r-- 2000-02-21 13:57 +0100 1052 Divides.thy
-rw-r--r-- 2000-02-21 13:57 +0100 26496 Finite.ML
-rw-r--r-- 2000-02-21 13:57 +0100 1802 Finite.thy
-rw-r--r-- 2000-02-21 13:57 +0100 15524 Fun.ML
-rw-r--r-- 2000-02-21 13:57 +0100 2639 Fun.thy
-rw-r--r-- 2000-02-21 13:57 +0100 4248 Gfp.ML
-rw-r--r-- 2000-02-21 13:57 +0100 362 Gfp.thy
-rw-r--r-- 2000-02-21 13:57 +0100 678 HOL.ML
-rw-r--r-- 2000-02-21 13:57 +0100 6353 HOL.thy
-rw-r--r-- 2000-02-21 13:57 +0100 13516 HOL_lemmas.ML
-rw-r--r-- 2000-02-21 13:57 +0100 583 Inductive.thy
-rw-r--r-- 2000-02-21 13:57 +0100 19203 IsaMakefile
-rw-r--r-- 2000-02-21 13:57 +0100 2420 Lfp.ML
-rw-r--r-- 2000-02-21 13:57 +0100 352 Lfp.thy
-rw-r--r-- 2000-02-21 13:57 +0100 37386 List.ML
-rw-r--r-- 2000-02-21 13:57 +0100 6015 List.thy
-rw-r--r-- 2000-02-21 13:57 +0100 135 Main.thy
-rw-r--r-- 2000-02-21 13:57 +0100 4823 Map.ML
-rw-r--r-- 2000-02-21 13:57 +0100 1671 Map.thy
-rw-r--r-- 2000-02-21 13:57 +0100 3081 Nat.ML
-rw-r--r-- 2000-02-21 13:57 +0100 473 Nat.thy
-rw-r--r-- 2000-02-21 13:57 +0100 14793 NatDef.ML
-rw-r--r-- 2000-02-21 13:57 +0100 1231 NatDef.thy
-rw-r--r-- 2000-02-21 13:57 +0100 249 Numeral.ML
-rw-r--r-- 2000-02-21 13:57 +0100 499 Numeral.thy
-rw-r--r-- 2000-02-21 13:57 +0100 1914 Option.ML
-rw-r--r-- 2000-02-21 13:57 +0100 517 Option.thy
-rw-r--r-- 2000-02-21 13:57 +0100 6812 Ord.ML
-rw-r--r-- 2000-02-21 13:57 +0100 2591 Ord.thy
-rw-r--r-- 2000-02-21 13:57 +0100 3184 Power.ML
-rw-r--r-- 2000-02-21 13:57 +0100 600 Power.thy
-rw-r--r-- 2000-02-21 13:57 +0100 16764 Prod.ML
-rw-r--r-- 2000-02-21 13:57 +0100 2804 Prod.thy
-rw-r--r-- 2000-02-21 13:57 +0100 2703 README.html
-rw-r--r-- 2000-02-21 13:57 +0100 977 ROOT.ML
-rw-r--r-- 2000-02-21 13:57 +0100 740 Recdef.thy
-rw-r--r-- 2000-02-21 13:57 +0100 1845 Record.thy
-rw-r--r-- 2000-02-21 13:57 +0100 3136 RelPow.ML
-rw-r--r-- 2000-02-21 13:57 +0100 317 RelPow.thy
-rw-r--r-- 2000-02-21 13:57 +0100 9797 Relation.ML
-rw-r--r-- 2000-02-21 13:57 +0100 1769 Relation.thy
-rw-r--r-- 2000-02-21 13:57 +0100 4720 SVC_Oracle.ML
-rw-r--r-- 2000-02-21 13:57 +0100 466 SVC_Oracle.thy
-rw-r--r-- 2000-02-21 13:57 +0100 19185 Set.ML
-rw-r--r-- 2000-02-21 13:57 +0100 7483 Set.thy
-rw-r--r-- 2000-02-21 13:57 +0100 3922 Sexp.ML
-rw-r--r-- 2000-02-21 13:57 +0100 1122 Sexp.thy
-rw-r--r-- 2000-02-21 13:57 +0100 2312 String.thy
-rw-r--r-- 2000-02-21 13:57 +0100 4477 Sum.ML
-rw-r--r-- 2000-02-21 13:57 +0100 1174 Sum.thy
-rw-r--r-- 2000-02-21 13:57 +0100 11842 Trancl.ML
-rw-r--r-- 2000-02-21 13:57 +0100 774 Trancl.thy
-rw-r--r-- 2000-02-21 13:57 +0100 15790 Univ.ML
-rw-r--r-- 2000-02-21 13:57 +0100 3509 Univ.thy
-rw-r--r-- 2000-02-21 13:57 +0100 2232 Vimage.ML
-rw-r--r-- 2000-02-21 13:57 +0100 355 Vimage.thy
-rw-r--r-- 2000-02-21 13:57 +0100 12543 WF.ML
-rw-r--r-- 2000-02-21 13:57 +0100 951 WF.thy
-rw-r--r-- 2000-02-21 13:57 +0100 7108 WF_Rel.ML
-rw-r--r-- 2000-02-21 13:57 +0100 1169 WF_Rel.thy
-rw-r--r-- 2000-02-21 13:57 +0100 1042 blastdata.ML
-rw-r--r-- 2000-02-21 13:57 +0100 1661 cladata.ML
-rw-r--r-- 2000-02-21 13:57 +0100 21777 equalities.ML
-rw-r--r-- 2000-02-21 13:57 +0100 258 equalities.thy
-rw-r--r-- 2000-02-21 13:57 +0100 6638 hologic.ML
-rw-r--r-- 2000-02-21 13:57 +0100 3148 mono.ML
-rw-r--r-- 2000-02-21 13:57 +0100 196 mono.thy
-rw-r--r-- 2000-02-21 13:57 +0100 18982 simpdata.ML
-rw-r--r-- 2000-02-21 13:57 +0100 2556 subset.ML
-rw-r--r-- 2000-02-21 13:57 +0100 271 subset.thy
-rw-r--r-- 2000-02-21 13:57 +0100 9504 thy_syntax.ML