src/HOL/Library/Library.thy
author wenzelm
Wed, 31 Aug 2005 15:46:38 +0200
changeset 17201 3bdf1dfcdee4
parent 16966 37e34f315057
child 17516 45164074dad4
permissions -rw-r--r--
reactivate postfix by change of syntax; tuned presentation;

(*<*)
theory Library
imports
  Accessible_Part
  BigO
  Continuity
  EfficientNat
  FuncSet
  Multiset
  NatPair
  Nat_Infinity
  Nested_Environment
  OptionalSugar
  Permutation
  Primes
  Quotient
  While_Combinator
  Word
  Zorn
  Char_ord
begin
end
(*>*)