/src/HOL/Library/
drwxr-xr-x [up]
drwxr-xr-x Library
-rw-r--r-- 2009-03-27 14:44 +0000 21401 Abstract_Rat.thy
-rw-r--r-- 2009-03-27 14:44 +0000 24439 AssocList.thy
-rw-r--r-- 2009-03-27 14:44 +0000 26477 BigO.thy
-rw-r--r-- 2009-03-27 14:44 +0000 18176 Binomial.thy
-rw-r--r-- 2009-03-27 14:44 +0000 2921 Bit.thy
-rw-r--r-- 2009-03-27 14:44 +0000 11238 Boolean_Algebra.thy
-rw-r--r-- 2009-03-27 14:44 +0000 7006 Char_nat.thy
-rw-r--r-- 2009-03-27 14:44 +0000 2514 Char_ord.thy
-rw-r--r-- 2009-03-27 14:44 +0000 775 Code_Char.thy
-rw-r--r-- 2009-03-27 14:44 +0000 1283 Code_Char_chr.thy
-rw-r--r-- 2009-03-27 14:44 +0000 8554 Code_Index.thy
-rw-r--r-- 2009-03-27 14:44 +0000 2940 Code_Integer.thy
-rw-r--r-- 2009-03-27 14:44 +0000 26900 Coinductive_List.thy
-rw-r--r-- 2009-03-27 14:44 +0000 10839 Commutative_Ring.thy
-rw-r--r-- 2009-03-27 14:44 +0000 22386 ContNotDenum.thy
-rw-r--r-- 2009-03-27 14:44 +0000 8662 Continuity.thy
-rw-r--r-- 2009-03-27 14:44 +0000 7313 Countable.thy
-rw-r--r-- 2009-03-27 14:44 +0000 48027 Determinants.thy
-rw-r--r-- 2009-03-27 14:44 +0000 4708 Diagonalize.thy
-rw-r--r-- 2009-03-27 14:44 +0000 13616 Efficient_Nat.thy
-rw-r--r-- 2009-03-27 14:44 +0000 14558 Enum.thy
-rw-r--r-- 2009-03-27 14:44 +0000 205147 Euclidean_Space.thy
-rw-r--r-- 2009-03-27 14:44 +0000 4138 Eval_Witness.thy
-rw-r--r-- 2009-03-27 14:44 +0000 7962 Executable_Set.thy
-rw-r--r-- 2009-03-27 14:44 +0000 3286 Finite_Cartesian_Product.thy
-rw-r--r-- 2009-03-27 14:44 +0000 60934 Float.thy
-rw-r--r-- 2009-03-27 14:44 +0000 95181 Formal_Power_Series.thy
-rw-r--r-- 2009-03-27 14:44 +0000 17755 FrechetDeriv.thy
-rw-r--r-- 2009-03-27 14:44 +0000 7020 FuncSet.thy
-rw-r--r-- 2009-03-27 14:44 +0000 49393 Fundamental_Theorem_Algebra.thy
-rw-r--r-- 2009-03-27 14:44 +0000 2159 Glbs.thy
-rw-r--r-- 2009-03-27 14:44 +0000 15721 Infinite_Set.thy
-rw-r--r-- 2009-03-27 14:44 +0000 10623 Inner_Product.thy
-rw-r--r-- 2009-03-27 14:44 +0000 3145 LaTeXsugar.thy
-rw-r--r-- 2009-03-27 14:44 +0000 349 Lattice_Syntax.thy
-rw-r--r-- 2009-03-27 14:44 +0000 817 Library.thy
-rw-r--r-- 2009-03-27 14:44 +0000 4065 ListVector.thy
-rw-r--r-- 2009-03-27 14:44 +0000 12702 List_Prefix.thy
-rw-r--r-- 2009-03-27 14:44 +0000 3203 List_lexord.thy
-rw-r--r-- 2009-03-27 14:44 +0000 4194 Mapping.thy
-rw-r--r-- 2009-03-27 14:44 +0000 54365 Multiset.thy
-rw-r--r-- 2009-03-27 14:44 +0000 12317 Nat_Infinity.thy
-rw-r--r-- 2009-03-27 14:44 +0000 6027 Nat_Int_Bij.thy
-rw-r--r-- 2009-03-27 14:44 +0000 16414 Nested_Environment.thy
-rw-r--r-- 2009-03-27 14:44 +0000 13284 Numeral_Type.thy
-rw-r--r-- 2009-03-27 14:44 +0000 3363 Option_ord.thy
-rw-r--r-- 2009-03-27 14:44 +0000 2538 OptionalSugar.thy
-rw-r--r-- 2009-03-27 14:44 +0000 3176 Order_Relation.thy
-rw-r--r-- 2009-03-27 14:44 +0000 6103 Permutation.thy
-rw-r--r-- 2009-03-27 14:44 +0000 36904 Permutations.thy
-rw-r--r-- 2009-03-27 14:44 +0000 55636 Pocklington.thy
-rw-r--r-- 2009-03-27 14:44 +0000 10519 Poly_Deriv.thy
-rw-r--r-- 2009-03-27 14:44 +0000 44175 Polynomial.thy
-rw-r--r-- 2009-03-27 14:44 +0000 33434 Primes.thy
-rw-r--r-- 2009-03-27 14:44 +0000 9272 Product_Vector.thy
-rw-r--r-- 2009-03-27 14:44 +0000 1330 Product_ord.thy
-rw-r--r-- 2009-03-27 14:44 +0000 2735 Product_plus.thy
-rw-r--r-- 2009-03-27 14:44 +0000 2886 Quickcheck.thy
-rw-r--r-- 2009-03-27 14:44 +0000 800 Quicksort.thy
-rw-r--r-- 2009-03-27 14:44 +0000 6440 Quotient.thy
-rw-r--r-- 2009-03-27 14:44 +0000 41390 RBT.thy
-rw-r--r-- 2009-03-27 14:44 +0000 4400 README.html
-rw-r--r-- 2009-03-27 14:44 +0000 12763 Ramsey.thy
-rw-r--r-- 2009-03-27 14:44 +0000 4538 Random.thy
-rw-r--r-- 2009-03-27 14:44 +0000 1328 Reflection.thy
-rw-r--r-- 2009-03-27 14:44 +0000 10823 SetsAndFunctions.thy
-rw-r--r-- 2009-03-27 14:44 +0000 6896 State_Monad.thy
-rw-r--r-- 2009-03-27 14:44 +0000 7817 Sublist_Order.thy
-rw-r--r-- 2009-03-27 14:44 +0000 297026 Topology_Euclidean_Space.thy
-rw-r--r-- 2009-03-27 14:44 +0000 39082 Univ_Poly.thy
-rw-r--r-- 2009-03-27 14:44 +0000 3509 While_Combinator.thy
-rw-r--r-- 2009-03-27 14:44 +0000 77657 Word.thy
-rw-r--r-- 2009-03-27 14:44 +0000 21080 Zorn.thy
-rw-r--r-- 2009-03-27 14:44 +0000 4404 comm_ring.ML
-rw-r--r-- 2009-03-27 14:44 +0000 48652 normarith.ML
-rw-r--r-- 2009-03-27 14:44 +0000 12655 reflection.ML
-rw-r--r-- 2009-03-27 14:44 +0000 1031 reify_data.ML