equal
deleted
inserted
replaced
4 val inj_repabs_trm: Proof.context -> (term * term) -> term |
4 val inj_repabs_trm: Proof.context -> (term * term) -> term |
5 end; |
5 end; |
6 |
6 |
7 structure Quotient_Term: QUOTIENT_TERM = |
7 structure Quotient_Term: QUOTIENT_TERM = |
8 struct |
8 struct |
|
9 |
|
10 open Quotient_Info; |
|
11 open Quotient_Type; |
|
12 open Quotient_Def; |
9 |
13 |
10 (* |
14 (* |
11 Regularizing an rtrm means: |
15 Regularizing an rtrm means: |
12 |
16 |
13 - Quantifiers over types that need lifting are replaced |
17 - Quantifiers over types that need lifting are replaced |