| changeset 89 | 42af13d194c9 |
| parent 88 | 1436fc451bb9 |
| child 91 | 37ab56205097 |
| 88:1436fc451bb9 | 89:42af13d194c9 |
|---|---|
350 unfolding quotient_def |
350 unfolding quotient_def |
351 by auto |
351 by auto |
352 |
352 |
353 |
353 |
354 section {* Equational systems *} |
354 section {* Equational systems *} |
355 |
|
356 |
|
357 text {* The two kinds of terms in the rhs of equations. *} |
|
355 |
358 |
356 datatype rhs_item = |
359 datatype rhs_item = |
357 Lam "rexp" (* Lambda-marker *) |
360 Lam "rexp" (* Lambda-marker *) |
358 | Trn "lang" "rexp" (* Transition *) |
361 | Trn "lang" "rexp" (* Transition *) |
359 |
362 |