equal
deleted
inserted
replaced
2 theory Paper |
2 theory Paper |
3 imports "Quotient" |
3 imports "Quotient" |
4 "LaTeXsugar" |
4 "LaTeXsugar" |
5 "../Nominal/FSet" |
5 "../Nominal/FSet" |
6 begin |
6 begin |
|
7 |
|
8 (**** |
|
9 |
|
10 ** things to do for the next version |
|
11 * |
|
12 * - what are quot_thms? |
|
13 * - what do all preservation theorems look like |
|
14 *) |
7 |
15 |
8 notation (latex output) |
16 notation (latex output) |
9 rel_conj ("_ \<circ>\<circ>\<circ> _" [53, 53] 52) and |
17 rel_conj ("_ \<circ>\<circ>\<circ> _" [53, 53] 52) and |
10 pred_comp ("_ \<circ>\<circ> _" [1, 1] 30) and |
18 pred_comp ("_ \<circ>\<circ> _" [1, 1] 30) and |
11 "op -->" (infix "\<longrightarrow>" 100) and |
19 "op -->" (infix "\<longrightarrow>" 100) and |