| author | oheimb |
| Thu, 24 Sep 1998 17:17:14 +0200 | |
| changeset 5553 | ae42b36a50c2 |
| parent 3059 | 3d7a61301137 |
| permissions | -rw-r--r-- |
| 2906 | 1 |
(* Title: HOL/Quot/FRACT.thy |
2 |
ID: $Id$ |
|
3 |
Author: Oscar Slotosch |
|
4 |
Copyright 1997 Technische Universitaet Muenchen |
|
5 |
||
| 2910 | 6 |
Example for higher order quotients: fractions |
| 2906 | 7 |
*) |
8 |
||
9 |
FRACT = NPAIR + HQUOT + |
|
10 |
instance |
|
11 |
NP::per |
|
|
3059
3d7a61301137
used explcite tactics in instances (since ax_per_trans "loops")
slotosch
parents:
2910
diff
changeset
|
12 |
{| (etac per_trans_NP 1) THEN (atac 1) THEN (etac per_sym_NP 1) |}
|
| 2906 | 13 |
|
14 |
(* now define fractions *) |
|
15 |
||
16 |
types fract = NP quot |
|
17 |
||
18 |
(* example for fractions *) |
|
19 |
consts |
|
20 |
half :: "fract" |
|
21 |
||
22 |
defs half_def "half == <[abs_NP(1,2)]>" |
|
|
3059
3d7a61301137
used explcite tactics in instances (since ax_per_trans "loops")
slotosch
parents:
2910
diff
changeset
|
23 |
end |