| changeset 2747 | a5da7b6aff8f |
| parent 2558 | 6cfb5d8a5b5b |
| child 2774 | d19bfc6e7631 |
| 2746:6aa98a113e6c | 2747:a5da7b6aff8f |
|---|---|
1 (*<*) |
1 (*<*) |
2 theory Paper |
2 theory Paper |
3 imports "Quotient" "Quotient_Syntax" |
3 imports "Quotient" "Quotient_Syntax" |
4 "LaTeXsugar" |
4 "~~/src/HOL/Library/LaTeXsugar" |
5 "$ISABELLE_HOME/src/HOL/Quotient_Examples/FSet" |
5 "~~/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 |