/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-- 1996-02-09 13:41 +0100 12479 Arith.ML
-rw-r--r-- 1996-02-09 13:41 +0100 979 Arith.thy
-rw-r--r-- 1996-02-09 13:41 +0100 2867 Finite.ML
-rw-r--r-- 1996-02-09 13:41 +0100 375 Finite.thy
-rw-r--r-- 1996-02-09 13:41 +0100 6016 Fun.ML
-rw-r--r-- 1996-02-09 13:41 +0100 206 Fun.thy
-rw-r--r-- 1996-02-09 13:41 +0100 4844 Gfp.ML
-rw-r--r-- 1996-02-09 13:41 +0100 350 Gfp.thy
-rw-r--r-- 1996-02-09 13:41 +0100 10902 HOL.ML
-rw-r--r-- 1996-02-09 13:41 +0100 4397 HOL.thy
-rw-r--r-- 1996-02-09 13:41 +0100 2655 Inductive.ML
-rw-r--r-- 1996-02-09 13:41 +0100 30 Inductive.thy
-rw-r--r-- 1996-02-09 13:41 +0100 3144 Lfp.ML
-rw-r--r-- 1996-02-09 13:41 +0100 340 Lfp.thy
-rw-r--r-- 1996-02-09 13:41 +0100 6159 List.ML
-rw-r--r-- 1996-02-09 13:41 +0100 2801 List.thy
-rw-r--r-- 1996-02-09 13:41 +0100 5674 Makefile
-rw-r--r-- 1996-02-09 13:41 +0100 14003 Nat.ML
-rw-r--r-- 1996-02-09 13:41 +0100 1471 Nat.thy
-rw-r--r-- 1996-02-09 13:41 +0100 536 Ord.ML
-rw-r--r-- 1996-02-09 13:41 +0100 637 Ord.thy
-rw-r--r-- 1996-02-09 13:41 +0100 8444 Prod.ML
-rw-r--r-- 1996-02-09 13:41 +0100 1921 Prod.thy
-rw-r--r-- 1996-02-09 13:41 +0100 795 README
-rw-r--r-- 1996-02-09 13:41 +0100 940 README.html
-rw-r--r-- 1996-02-09 13:41 +0100 929 ROOT.ML
-rw-r--r-- 1996-02-09 13:41 +0100 5031 Relation.ML
-rw-r--r-- 1996-02-09 13:41 +0100 1150 Relation.thy
-rw-r--r-- 1996-02-09 13:41 +0100 13928 Set.ML
-rw-r--r-- 1996-02-09 13:41 +0100 5036 Set.thy
-rw-r--r-- 1996-02-09 13:41 +0100 4778 Sexp.ML
-rw-r--r-- 1996-02-09 13:41 +0100 1090 Sexp.thy
-rw-r--r-- 1996-02-09 13:41 +0100 6228 Sum.ML
-rw-r--r-- 1996-02-09 13:41 +0100 1460 Sum.thy
-rw-r--r-- 1996-02-09 13:41 +0100 6999 Trancl.ML
-rw-r--r-- 1996-02-09 13:41 +0100 720 Trancl.thy
-rw-r--r-- 1996-02-09 13:41 +0100 17986 Univ.ML
-rw-r--r-- 1996-02-09 13:41 +0100 3175 Univ.thy
-rw-r--r-- 1996-02-09 13:41 +0100 7893 WF.ML
-rw-r--r-- 1996-02-09 13:41 +0100 931 WF.thy
-rw-r--r-- 1996-02-09 13:41 +0100 9369 add_ind_def.ML
-rw-r--r-- 1996-02-09 13:41 +0100 18615 datatype.ML
-rw-r--r-- 1996-02-09 13:41 +0100 8301 equalities.ML
-rw-r--r-- 1996-02-09 13:41 +0100 258 equalities.thy
-rw-r--r-- 1996-02-09 13:41 +0100 2060 hologic.ML
-rw-r--r-- 1996-02-09 13:41 +0100 4533 ind_syntax.ML
-rw-r--r-- 1996-02-09 13:41 +0100 8427 indrule.ML
-rw-r--r-- 1996-02-09 13:41 +0100 5345 intr_elim.ML
-rw-r--r-- 1996-02-09 13:41 +0100 3511 mono.ML
-rw-r--r-- 1996-02-09 13:41 +0100 196 mono.thy
-rw-r--r-- 1996-02-09 13:41 +0100 6096 simpdata.ML
-rw-r--r-- 1996-02-09 13:41 +0100 3853 subset.ML
-rw-r--r-- 1996-02-09 13:41 +0100 192 subset.thy
-rw-r--r-- 1996-02-09 13:41 +0100 450 thy_data.ML
-rw-r--r-- 1996-02-09 13:41 +0100 6844 thy_syntax.ML
-rw-r--r-- 1996-02-09 13:41 +0100 4180 typedef.ML