changeset 41144 | 509e51b7509a |
parent 37325 | c2a44bc874f9 |
child 42103 | 6066a35f6678 |
41143:0b05cc14c2cb | 41144:509e51b7509a |
---|---|
1 (* Title: HOL/Metis_Examples/set.thy |
1 (* Title: HOL/Metis_Examples/set.thy |
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 |
3 Author: Jasmin Blanchette, TU Muenchen |
4 Testing the metis method. |
4 |
5 Testing Metis. |
|
5 *) |
6 *) |
6 |
7 |
7 theory set |
8 theory set |
8 imports Main |
9 imports Main |
9 begin |
10 begin |