| changeset 2551 | 26d594a9b89f |
| parent 2549 | c9f71476b030 |
| child 2552 | bf4b28ebb412 |
| 2550:551c5a8b6b2c | 2551:26d594a9b89f |
|---|---|
1 (*<*) |
1 (*<*) |
2 theory Paper |
2 theory Paper |
3 imports "Quotient" "Quotient_Syntax" |
3 imports "Quotient" "Quotient_Syntax" |
4 "LaTeXsugar" |
4 "LaTeXsugar" |
5 "../Nominal/FSet" |
5 "$ISABELLE_HOME/src/HOL/Quotient_Examples/FSet" |
6 begin |
6 begin |
7 |
7 |
8 (**** |
8 (**** |
9 |
9 |
10 ** things to do for the next version |
10 ** things to do for the next version |