changeset 67006 | b1278ed3cd46 |
parent 66453 | cc19f7ca2ed6 |
child 67398 | 5eb932e604a2 |
67005:11fca474d87a | 67006:b1278ed3cd46 |
---|---|
1 (* Author: Florian Haftmann, TU Muenchen *) |
1 (* Author: Florian Haftmann, TU Muenchen *) |
2 |
2 |
3 section \<open>Preorders with explicit equivalence relation\<close> |
3 section \<open>Preorders with explicit equivalence relation\<close> |
4 |
4 |
5 theory Preorder |
5 theory Preorder |
6 imports HOL.Orderings |
6 imports Main |
7 begin |
7 begin |
8 |
8 |
9 class preorder_equiv = preorder |
9 class preorder_equiv = preorder |
10 begin |
10 begin |
11 |
11 |