src/HOL/Library/Library.thy
author nipkow
Sun, 09 Apr 2006 19:41:30 +0200
changeset 19390 6c7383f80ad1
parent 19351 c33563c7c14c
child 19469 958d2f2dd8d4
permissions -rw-r--r--
Added function "splice"

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