Quotient-Paper/Paper.thy
author Christian Urban <urbanc@in.tum.de>
Thu, 29 Apr 2010 09:13:18 +0200
changeset 1975 b1281a0051ae
child 1978 8feedc0d4ea8
permissions -rw-r--r--
added stub for quotient paper; call with isabelle make qpaper
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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
(*>*)