author | paulson |
Wed, 07 Nov 2001 18:12:12 +0100 | |
changeset 12089 | 34e7693271a9 |
child 12190 | 32a9c240f225 |
permissions | -rw-r--r-- |
12089
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
1 |
(* Title: ZF/ex/ROOT |
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
2 |
ID: $Id$ |
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
4 |
Copyright 2001 University of Cambridge |
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
5 |
|
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
6 |
Inductive definitions |
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
7 |
*) |
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
8 |
|
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
9 |
(*by Sidi Ehmety: Multisets. A parent is FoldSet, the "fold" function for |
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
10 |
finite sets*) |
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
11 |
time_use_thy "Multiset"; |
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
12 |
|
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
13 |
time_use_thy "Rmap"; (*mapping a relation over a list*) |
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
14 |
time_use_thy "Mutil"; (*mutilated chess board*) |
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
15 |
time_use_thy "PropLog"; (*completeness of propositional logic*) |
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
16 |
|
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
17 |
(*two Coq examples by Christine Paulin-Mohring*) |
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
18 |
time_use_thy "ListN"; |
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
19 |
time_use_thy "Acc"; |
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
20 |
|
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
21 |
time_use_thy "Comb"; (*Combinatory Logic example*) |
34e7693271a9
Sidi Ehmety's port of the fold_set operator and multisets to ZF.
paulson
parents:
diff
changeset
|
22 |
time_use_thy "Primrec"; (*Primitive recursive functions*) |