/src/HOL/
drwxr-xr-x [up]
drwxr-xr-x AxClasses
drwxr-xr-x Hoare
drwxr-xr-x IMP
drwxr-xr-x IOA
drwxr-xr-x Integ
drwxr-xr-x Lambda
drwxr-xr-x Lex
drwxr-xr-x MiniML
drwxr-xr-x Subst
drwxr-xr-x ex
-rw-r--r-- 1995-12-11 11:24 +0100 12242 Arith.ML
-rw-r--r-- 1995-12-11 11:24 +0100 932 Arith.thy
-rw-r--r-- 1995-12-11 11:24 +0100 2692 Finite.ML
-rw-r--r-- 1995-12-11 11:24 +0100 368 Finite.thy
-rw-r--r-- 1995-12-11 11:24 +0100 5974 Fun.ML
-rw-r--r-- 1995-12-11 11:24 +0100 199 Fun.thy
-rw-r--r-- 1995-12-11 11:24 +0100 4795 Gfp.ML
-rw-r--r-- 1995-12-11 11:24 +0100 343 Gfp.thy
-rw-r--r-- 1995-12-11 11:24 +0100 9234 HOL.ML
-rw-r--r-- 1995-12-11 11:24 +0100 4397 HOL.thy
-rw-r--r-- 1995-12-11 11:24 +0100 2365 Inductive.ML
-rw-r--r-- 1995-12-11 11:24 +0100 30 Inductive.thy
-rw-r--r-- 1995-12-11 11:24 +0100 3004 Lfp.ML
-rw-r--r-- 1995-12-11 11:24 +0100 333 Lfp.thy
-rw-r--r-- 1995-12-11 11:24 +0100 6360 List.ML
-rw-r--r-- 1995-12-11 11:24 +0100 2736 List.thy
-rw-r--r-- 1995-12-11 11:24 +0100 5674 Makefile
-rw-r--r-- 1995-12-11 11:24 +0100 13426 Nat.ML
-rw-r--r-- 1995-12-11 11:24 +0100 1506 Nat.thy
-rw-r--r-- 1995-12-11 11:24 +0100 529 Ord.ML
-rw-r--r-- 1995-12-11 11:24 +0100 637 Ord.thy
-rw-r--r-- 1995-12-11 11:24 +0100 8075 Prod.ML
-rw-r--r-- 1995-12-11 11:24 +0100 2724 Prod.thy
-rw-r--r-- 1995-12-11 11:24 +0100 795 README
-rw-r--r-- 1995-12-11 11:24 +0100 940 README.html
-rw-r--r-- 1995-12-11 11:24 +0100 929 ROOT.ML
-rw-r--r-- 1995-12-11 11:24 +0100 5029 Relation.ML
-rw-r--r-- 1995-12-11 11:24 +0100 1196 Relation.thy
-rw-r--r-- 1995-12-11 11:24 +0100 13907 Set.ML
-rw-r--r-- 1995-12-11 11:24 +0100 5036 Set.thy
-rw-r--r-- 1995-12-11 11:24 +0100 4252 Sexp.ML
-rw-r--r-- 1995-12-11 11:24 +0100 1085 Sexp.thy
-rw-r--r-- 1995-12-11 11:24 +0100 6158 Sum.ML
-rw-r--r-- 1995-12-11 11:24 +0100 1459 Sum.thy
-rw-r--r-- 1995-12-11 11:24 +0100 6870 Trancl.ML
-rw-r--r-- 1995-12-11 11:24 +0100 704 Trancl.thy
-rw-r--r-- 1995-12-11 11:24 +0100 17809 Univ.ML
-rw-r--r-- 1995-12-11 11:24 +0100 3175 Univ.thy
-rw-r--r-- 1995-12-11 11:24 +0100 6549 WF.ML
-rw-r--r-- 1995-12-11 11:24 +0100 925 WF.thy
-rw-r--r-- 1995-12-11 11:24 +0100 8831 add_ind_def.ML
-rw-r--r-- 1995-12-11 11:24 +0100 17242 datatype.ML
-rw-r--r-- 1995-12-11 11:24 +0100 8294 equalities.ML
-rw-r--r-- 1995-12-11 11:24 +0100 251 equalities.thy
-rw-r--r-- 1995-12-11 11:24 +0100 2060 hologic.ML
-rw-r--r-- 1995-12-11 11:24 +0100 4214 ind_syntax.ML
-rw-r--r-- 1995-12-11 11:24 +0100 6999 indrule.ML
-rw-r--r-- 1995-12-11 11:24 +0100 4867 intr_elim.ML
-rw-r--r-- 1995-12-11 11:24 +0100 3490 mono.ML
-rw-r--r-- 1995-12-11 11:24 +0100 189 mono.thy
-rw-r--r-- 1995-12-11 11:24 +0100 5943 simpdata.ML
-rw-r--r-- 1995-12-11 11:24 +0100 3783 subset.ML
-rw-r--r-- 1995-12-11 11:24 +0100 185 subset.thy
-rw-r--r-- 1995-12-11 11:24 +0100 4180 subtype.ML
-rw-r--r-- 1995-12-11 11:24 +0100 6644 thy_syntax.ML
-rw-r--r-- 1995-12-11 11:24 +0100 4180 typedef.ML