| changeset 2910 | 905aa895136c |
| parent 2906 | 171dedbc9bdb |
| child 3059 | 3d7a61301137 |
| 2909:22a8a97b66be | 2910:905aa895136c |
|---|---|
1 (* Title: HOL/Quot/FRACT.thy |
1 (* Title: HOL/Quot/FRACT.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Oscar Slotosch |
3 Author: Oscar Slotosch |
4 Copyright 1997 Technische Universitaet Muenchen |
4 Copyright 1997 Technische Universitaet Muenchen |
5 |
5 |
6 Example for higher order quotients: fractionals |
6 Example for higher order quotients: fractions |
7 *) |
7 *) |
8 |
8 |
9 FRACT = NPAIR + HQUOT + |
9 FRACT = NPAIR + HQUOT + |
10 instance |
10 instance |
11 NP::per |
11 NP::per |