| changeset 774 | b4ffb8826105 |
| parent 773 | d6acae26d027 |
| child 775 | 26fefde1d124 |
| 773:d6acae26d027 | 774:b4ffb8826105 |
|---|---|
10 |
10 |
11 structure Quotient_Tacs: QUOTIENT_TACS = |
11 structure Quotient_Tacs: QUOTIENT_TACS = |
12 struct |
12 struct |
13 |
13 |
14 open Quotient_Info; |
14 open Quotient_Info; |
15 open Quotient_Type; |
|
16 open Quotient_Term; |
15 open Quotient_Term; |
17 |
16 |
18 |
17 |
19 (* Since HOL_basic_ss is too "big" for us, we *) |
18 (* Since HOL_basic_ss is too "big" for us, we *) |
20 (* need to set up our own minimal simpset. *) |
19 (* need to set up our own minimal simpset. *) |