/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 Hyperreal
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 Lattice
drwxr-xr-x Lex
drwxr-xr-x Library
drwxr-xr-x MicroJava
drwxr-xr-x MiniML
drwxr-xr-x Modelcheck
drwxr-xr-x NumberTheory
drwxr-xr-x Prolog
drwxr-xr-x Real
drwxr-xr-x Subst
drwxr-xr-x TLA
drwxr-xr-x Tools
drwxr-xr-x UNITY
drwxr-xr-x Unix
drwxr-xr-x W0
drwxr-xr-x ex
-rw-r--r-- 2001-02-02 22:18 +0100 5141 Calculation.thy
-rw-r--r-- 2001-02-02 22:18 +0100 1039 Datatype.ML
-rw-r--r-- 2001-02-02 22:18 +0100 450 Datatype.thy
-rw-r--r-- 2001-02-02 22:18 +0100 15374 Datatype_Universe.ML
-rw-r--r-- 2001-02-02 22:18 +0100 3504 Datatype_Universe.thy
-rw-r--r-- 2001-02-02 22:18 +0100 20269 Divides.ML
-rw-r--r-- 2001-02-02 22:18 +0100 1424 Divides.thy
-rw-r--r-- 2001-02-02 22:18 +0100 28264 Finite.ML
-rw-r--r-- 2001-02-02 22:18 +0100 1828 Finite.thy
-rw-r--r-- 2001-02-02 22:18 +0100 18349 Fun.ML
-rw-r--r-- 2001-02-02 22:18 +0100 2903 Fun.thy
-rw-r--r-- 2001-02-02 22:18 +0100 3857 Gfp.ML
-rw-r--r-- 2001-02-02 22:18 +0100 347 Gfp.thy
-rw-r--r-- 2001-02-02 22:18 +0100 764 HOL.ML
-rw-r--r-- 2001-02-02 22:18 +0100 7625 HOL.thy
-rw-r--r-- 2001-02-02 22:18 +0100 11776 HOL_lemmas.ML
-rw-r--r-- 2001-02-02 22:18 +0100 2607 Inductive.thy
-rw-r--r-- 2001-02-02 22:18 +0100 2348 Inverse_Image.ML
-rw-r--r-- 2001-02-02 22:18 +0100 344 Inverse_Image.thy
-rw-r--r-- 2001-02-02 22:18 +0100 20660 IsaMakefile
-rw-r--r-- 2001-02-02 22:18 +0100 2417 Lfp.ML
-rw-r--r-- 2001-02-02 22:18 +0100 345 Lfp.thy
-rw-r--r-- 2001-02-02 22:18 +0100 38007 List.ML
-rw-r--r-- 2001-02-02 22:18 +0100 6202 List.thy
-rw-r--r-- 2001-02-02 22:18 +0100 58 Main.ML
-rw-r--r-- 2001-02-02 22:18 +0100 435 Main.thy
-rw-r--r-- 2001-02-02 22:18 +0100 6217 Map.ML
-rw-r--r-- 2001-02-02 22:18 +0100 1574 Map.thy
-rw-r--r-- 2001-02-02 22:18 +0100 21057 Nat.ML
-rw-r--r-- 2001-02-02 22:18 +0100 995 Nat.thy
-rw-r--r-- 2001-02-02 22:18 +0100 3496 NatArith.ML
-rw-r--r-- 2001-02-02 22:18 +0100 475 NatArith.thy
-rw-r--r-- 2001-02-02 22:18 +0100 13349 NatDef.ML
-rw-r--r-- 2001-02-02 22:18 +0100 1217 NatDef.thy
-rw-r--r-- 2001-02-02 22:18 +0100 573 Numeral.ML
-rw-r--r-- 2001-02-02 22:18 +0100 498 Numeral.thy
-rw-r--r-- 2001-02-02 22:18 +0100 2016 Option.ML
-rw-r--r-- 2001-02-02 22:18 +0100 482 Option.thy
-rw-r--r-- 2001-02-02 22:18 +0100 7082 Ord.ML
-rw-r--r-- 2001-02-02 22:18 +0100 2604 Ord.thy
-rw-r--r-- 2001-02-02 22:18 +0100 3278 Power.ML
-rw-r--r-- 2001-02-02 22:18 +0100 608 Power.thy
-rw-r--r-- 2001-02-02 22:18 +0100 1254 PreList.thy
-rw-r--r-- 2001-02-02 22:18 +0100 3460 Product_Type.thy
-rw-r--r-- 2001-02-02 22:18 +0100 17077 Product_Type_lemmas.ML
-rw-r--r-- 2001-02-02 22:18 +0100 2965 README.html
-rw-r--r-- 2001-02-02 22:18 +0100 1149 ROOT.ML
-rw-r--r-- 2001-02-02 22:18 +0100 1645 Recdef.thy
-rw-r--r-- 2001-02-02 22:18 +0100 3120 Record.thy
-rw-r--r-- 2001-02-02 22:18 +0100 10416 Relation.ML
-rw-r--r-- 2001-02-02 22:18 +0100 1959 Relation.thy
-rw-r--r-- 2001-02-02 22:18 +0100 3140 Relation_Power.ML
-rw-r--r-- 2001-02-02 22:18 +0100 342 Relation_Power.thy
-rw-r--r-- 2001-02-02 22:18 +0100 4720 SVC_Oracle.ML
-rw-r--r-- 2001-02-02 22:18 +0100 466 SVC_Oracle.thy
-rw-r--r-- 2001-02-02 22:18 +0100 20050 Set.ML
-rw-r--r-- 2001-02-02 22:18 +0100 7364 Set.thy
-rw-r--r-- 2001-02-02 22:18 +0100 3770 SetInterval.ML
-rw-r--r-- 2001-02-02 22:18 +0100 515 SetInterval.thy
-rw-r--r-- 2001-02-02 22:18 +0100 2809 String.thy
-rw-r--r-- 2001-02-02 22:18 +0100 4505 Sum.ML
-rw-r--r-- 2001-02-02 22:18 +0100 4510 Sum_Type.ML
-rw-r--r-- 2001-02-02 22:18 +0100 1195 Sum_Type.thy
-rw-r--r-- 2001-02-02 22:18 +0100 2619 Transitive_Closure.thy
-rw-r--r-- 2001-02-02 22:18 +0100 11400 Transitive_Closure_lemmas.ML
-rw-r--r-- 2001-02-02 22:18 +0100 12365 Wellfounded_Recursion.ML
-rw-r--r-- 2001-02-02 22:18 +0100 987 Wellfounded_Recursion.thy
-rw-r--r-- 2001-02-02 22:18 +0100 7814 Wellfounded_Relations.ML
-rw-r--r-- 2001-02-02 22:18 +0100 1390 Wellfounded_Relations.thy
-rw-r--r-- 2001-02-02 22:18 +0100 13829 arith_data.ML
-rw-r--r-- 2001-02-02 22:18 +0100 1072 blastdata.ML
-rw-r--r-- 2001-02-02 22:18 +0100 2194 cladata.ML
-rw-r--r-- 2001-02-02 22:18 +0100 22152 equalities.ML
-rw-r--r-- 2001-02-02 22:18 +0100 258 equalities.thy
-rw-r--r-- 2001-02-02 22:18 +0100 7999 hologic.ML
-rw-r--r-- 2001-02-02 22:18 +0100 2477 meson_lemmas.ML
-rw-r--r-- 2001-02-02 22:18 +0100 3141 mono.ML
-rw-r--r-- 2001-02-02 22:18 +0100 196 mono.thy
-rw-r--r-- 2001-02-02 22:18 +0100 16263 simpdata.ML
-rw-r--r-- 2001-02-02 22:18 +0100 2556 subset.ML
-rw-r--r-- 2001-02-02 22:18 +0100 3742 subset.thy
-rw-r--r-- 2001-02-02 22:18 +0100 9841 thy_syntax.ML