author | Christian Urban <urbanc@in.tum.de> |
Thu, 29 Apr 2010 10:16:15 +0200 | |
changeset 1979 | 760257a66604 |
parent 1975 | b1281a0051ae |
child 1978 | 8feedc0d4ea8 |
permissions | -rw-r--r-- |
1975
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
1 |
(*<*) |
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
2 |
theory Paper |
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
3 |
imports "Quotient" |
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
4 |
"LaTeXsugar" |
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
5 |
begin |
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
6 |
(*>*) |
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
7 |
|
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
8 |
section {* Introduction *} |
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
9 |
|
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
10 |
text {* TBD *} |
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
11 |
|
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
12 |
|
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
13 |
|
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
14 |
(*<*) |
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
15 |
end |
b1281a0051ae
added stub for quotient paper; call with isabelle make qpaper
Christian Urban <urbanc@in.tum.de>
parents:
diff
changeset
|
16 |
(*>*) |