src/HOL/Quotient_Examples/FSet.thy
changeset 41467 8fc17c5e11c0
parent 41413 64cd30d6b0b8
child 44204 3cdc4176638c
equal deleted inserted replaced
41466:73981e95b30b 41467:8fc17c5e11c0
     1 (*  Title:      HOL/Quotient_Examples/FSet.thy
     1 (*  Title:      HOL/Quotient_Examples/FSet.thy
     2     Author:     Cezary Kaliszyk, TU Munich
     2     Author:     Cezary Kaliszyk, TU Munich
     3     Author:     Christian Urban, TU Munich
     3     Author:     Christian Urban, TU Munich
     4 
     4 
     5     Type of finite sets.
     5 Type of finite sets.
     6 *)
     6 *)
     7 
     7 
     8 theory FSet
     8 theory FSet
     9 imports "~~/src/HOL/Library/Quotient_List" "~~/src/HOL/Library/More_List"
     9 imports "~~/src/HOL/Library/Quotient_List" "~~/src/HOL/Library/More_List"
    10 begin
    10 begin