equal
deleted
inserted
replaced
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" |
10 begin |
10 begin |
11 |
11 |
12 text {* |
12 text {* |
13 The type of finite sets is created by a quotient construction |
13 The type of finite sets is created by a quotient construction |
14 over lists. The definition of the equivalence: |
14 over lists. The definition of the equivalence: |