equal
deleted
inserted
replaced
1086 rsp/prs databases) and programatically (automated definition of |
1086 rsp/prs databases) and programatically (automated definition of |
1087 lifted constants, the rsp proof obligations and theorem statement |
1087 lifted constants, the rsp proof obligations and theorem statement |
1088 translation according to given quotients). |
1088 translation according to given quotients). |
1089 |
1089 |
1090 \end{itemize} |
1090 \end{itemize} |
|
1091 |
|
1092 \medskip |
|
1093 \noindent |
|
1094 {\bf Acknowledgements:} We would like to thank Peter Homeier for the |
|
1095 discussions about the HOL4 quotient package and explaining us its |
|
1096 implementation details. |
|
1097 |
1091 *} |
1098 *} |
1092 |
1099 |
1093 |
1100 |
1094 |
1101 |
1095 (*<*) |
1102 (*<*) |