src/HOL/Library/SetsAndFunctions.thy
changeset 30738 0842e906300c
parent 29667 53103fc8ffa3
child 30741 9e23e3ea7edd
equal deleted inserted replaced
30737:9ffd27558916 30738:0842e906300c
     3 *)
     3 *)
     4 
     4 
     5 header {* Operations on sets and functions *}
     5 header {* Operations on sets and functions *}
     6 
     6 
     7 theory SetsAndFunctions
     7 theory SetsAndFunctions
     8 imports Plain
     8 imports Main
     9 begin
     9 begin
    10 
    10 
    11 text {*
    11 text {*
    12 This library lifts operations like addition and muliplication to sets and
    12 This library lifts operations like addition and muliplication to sets and
    13 functions of appropriate types. It was designed to support asymptotic
    13 functions of appropriate types. It was designed to support asymptotic