diff --git a/kwarcbibs.sty b/kwarcbibs.sty
new file mode 100644
index 0000000000000000000000000000000000000000..8363a436efc5cdc6e6fb339fa8e60d0b154bd351
--- /dev/null
+++ b/kwarcbibs.sty
@@ -0,0 +1,40 @@
+\RequirePackage{url}
+\providecommand\seen{seen }
+\providecommand\selfedit{}
+\providecommand\webpageat{web page at }
+\providecommand\homepageat{home page at }
+\providecommand\projectpageat{project page at }
+\providecommand\systempageat{system home page at }
+\providecommand\svnrepoat{Subversion repository at }
+\providecommand\January{January}
+\providecommand\February{February}
+\providecommand\Feb{February}
+\providecommand\March{March}
+\providecommand\April{April}
+\providecommand\May{May}
+\providecommand\June{June}
+\providecommand\July{July}
+\providecommand\August{August}
+\providecommand\September{September}
+\providecommand\October{October}
+\providecommand\November{November}
+\providecommand\December{December}
+\providecommand\AUSTRALIA{Australia}
+\providecommand\ROMANIA{Romania}
+\providecommand\MEXICO{Mexico}
+\providecommand\ITALY{Italy}
+\providecommand\USA{USA}
+\providecommand\IRELAND{Ireland}
+\providecommand\HUNGARY{Hungary}
+\providecommand\JAPAN{Japan}
+\providecommand\CANADA{Canada}
+\providecommand\SPAIN{Spain}
+\providecommand\NETHERLANDS{Netherlands}
+\providecommand\UK{UK}
+\providecommand\SWEDEN{Sweden}
+\providecommand\GERMANY{Germany}
+\providecommand\openmath{OpenMath}
+\providecommand\fc{forthcoming}
+\providecommand\PROC{Proceedings}
+\providecommand\omdoc{OMDoc}
+\providecommand\activemath{ActiveMath}
diff --git a/marvosym.sty.ltxml b/marvosym.sty.ltxml
new file mode 100755
index 0000000000000000000000000000000000000000..9ab564fab970971c5ca08d9aa6a2553aa0d60ae6
--- /dev/null
+++ b/marvosym.sty.ltxml
@@ -0,0 +1,17 @@
+# -*- CPERL -*-
+# /=======================================================\ #
+# | marvosym.sty - Implementation for LaTeXML | #
+# | | #
+# |=======================================================| #
+# | Not Part of LaTeXML : http://dlmf.nist.gov/LaTeXML/ | #
+# | Copyright (c) 2006 arXMLiv group | #
+# | Released under the GNU Public License | #
+# \=======================================================/ #
+
+package LaTeXML::Package::Pool;
+use strict;
+use LaTeXML::Package;
+
+DefMacro('\EUR', "\x{20AC}");
+#**********************************************************************
+1;
diff --git a/pgflibrarytikzdocicon.code.tex b/pgflibrarytikzdocicon.code.tex
new file mode 100755
index 0000000000000000000000000000000000000000..696efd0c6c8dc429bedaf7f31ab88744e94348a0
--- /dev/null
+++ b/pgflibrarytikzdocicon.code.tex
@@ -0,0 +1,44 @@
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% A TIKZ module for document icons code copied (thanks) from
+% http://tex.stackexchange.com/questions/103688/folded-paper-shape-tikz
+% use e.g. as
+% \tikzstyle{doc}=[draw,thick,align=center,color=black,
+% shape=document,minimum width=10mm,minimum height=15mm]
+% \node[doc] (d0) at (-1,0) {};
+% \node[doc] at (0,0) {Annotation}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+\pgfdeclareshape{document}{
+\inheritsavedanchors[from=rectangle] % this is nearly a rectangle
+\inheritanchorborder[from=rectangle]
+\inheritanchor[from=rectangle]{center}
+\inheritanchor[from=rectangle]{north}
+\inheritanchor[from=rectangle]{south}
+\inheritanchor[from=rectangle]{west}
+\inheritanchor[from=rectangle]{east}
+% ... and possibly more
+\backgroundpath{% this is new
+% store lower right in xa/ya and upper right in xb/yb
+\southwest \pgf@xa=\pgf@x \pgf@ya=\pgf@y
+\northeast \pgf@xb=\pgf@x \pgf@yb=\pgf@y
+% compute corner of ‘‘flipped page’’
+\pgf@xc=\pgf@xb \advance\pgf@xc by-5pt % this should be a parameter
+\pgf@yc=\pgf@yb \advance\pgf@yc by-5pt
+% construct main path
+\pgfpathmoveto{\pgfpoint{\pgf@xa}{\pgf@ya}}
+\pgfpathlineto{\pgfpoint{\pgf@xa}{\pgf@yb}}
+\pgfpathlineto{\pgfpoint{\pgf@xc}{\pgf@yb}}
+\pgfpathlineto{\pgfpoint{\pgf@xb}{\pgf@yc}}
+\pgfpathlineto{\pgfpoint{\pgf@xb}{\pgf@ya}}
+\pgfpathclose
+% add little corner
+\pgfpathmoveto{\pgfpoint{\pgf@xc}{\pgf@yb}}
+\pgfpathlineto{\pgfpoint{\pgf@xc}{\pgf@yc}}
+\pgfpathlineto{\pgfpoint{\pgf@xb}{\pgf@yc}}
+\pgfpathlineto{\pgfpoint{\pgf@xc}{\pgf@yc}}
+}
+}
+\def\dociconprototype#1{\raisebox{-.5ex}{\tikz{\node[draw,thick,shape=document,inner sep =
+3pt]{#1};}}}
+\makeatother
+
diff --git a/pgflibrarytikzmmt.code.tex b/pgflibrarytikzmmt.code.tex
new file mode 100755
index 0000000000000000000000000000000000000000..cd7a05ae02fd451afeeb7702c68e8ee48e1c2e2b
--- /dev/null
+++ b/pgflibrarytikzmmt.code.tex
@@ -0,0 +1,171 @@
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% A TIKZ library for MMT Theory Graphs
+% copyright 2014 Michael Kohlhase; Released under the LPPL
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%
+% this library provides some standardized node and arrow styles for formatting MMT graph
+% diagrams in tikz. The advantage is that we can classify the arrows and nodes
+% symbolically and with the styles in this library achieve a uniform look that helps
+% readability.
+%
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%% 1. Theories
+% a generic theory
+\def\outerthysep{.3mm}
+\def\innerthysep{.5mm}
+\tikzstyle{thy}=[draw,outer sep=\outerthysep,rounded corners,inner sep=\innerthysep]
+% a primitive theory
+\tikzstyle{primthy}=[thy,double]
+% a theory graph
+\tikzstyle{thygraph}=[draw,outer sep=1mm,rounded corners,dashed]
+
+%%% 2. Arrows
+%%% 2.1. Arrowtips (only internal)
+\usetikzlibrary{arrows}
+\newcommand{\@mmtarrowtip}{angle 45}
+\newcommand{\@mmtreversearrowtip}{angle 45 reversed}
+\newcommand{\@mmtarrowtipepi}{triangle 45}
+\newcommand{\@mmtarrowtipmonoright}{right hook}
+\newcommand{\@mmtarrowtipmonoleft}{left hook}
+\newcommand{\@mmtarrowtippartial}{right to}
+\newcommand{\@mmtarrowtippartialleft}{left to}
+\newcommand{\@mmtreversearrowtippartial}{right to reversed}
+\newcommand{\@mmtreversearrowtippartialleft}{left to reversed}
+
+%%% 2.2 the arrow sstyles in graphs
+\usetikzlibrary{decorations,decorations.pathmorphing,decorations.markings}
+% any morphism
+\tikzstyle{morph}=[-\@mmtarrowtip,thick]
+\tikzstyle{mapsto}=[|-\@mmtarrowtip] %| any morphism
+% structures
+\tikzstyle{struct}=[-\@mmtarrowtip,thick]
+% inclusions: regular, partial, and left variants
+\tikzstyle{include}=[\@mmtarrowtipmonoright-\@mmtarrowtip,thick]
+\tikzstyle{revinclude}=[\@mmtarrowtip-\@mmtarrowtipmonoright,thick]
+\tikzstyle{pinclude}=[\@mmtarrowtipmonoright-\@mmtarrowtippartial,thick]
+\tikzstyle{includeleft}=[\@mmtarrowtipmonoleft-\@mmtarrowtip,thick]
+\tikzstyle{pincludeleft}=[\@mmtarrowtipmonoleft-\@mmtarrowtippartialleft,thick]
+% views: regular, mono, partial, and left variants
+\tikzstyle{preview}=[decorate,
+ decoration={coil,aspect=0,amplitude=1pt,
+ segment length=6pt,
+ pre=lineto,pre length=3pt,
+ post=lineto,post length=5pt},
+ thick]
+\tikzstyle{view}=[preview,-\@mmtarrowtip]
+\tikzstyle{mview}=[preview,\@mmtarrowtipmonoright-\@mmtarrowtip]
+\tikzstyle{pview}=[preview,-\@mmtarrowtippartial]
+\tikzstyle{pmview}=[preview,\@mmtarrowtipmonoright-\@mmtarrowtippartial]
+\tikzstyle{viewleft}=[preview,-\@mmtarrowtip]
+\tikzstyle{mviewleft}=[preview,\@mmtarrowtipmonoleft-\@mmtarrowtip]
+\tikzstyle{pviewleft}=[preview,-\@mmtarrowtippartialleft]
+\tikzstyle{pmviewleft}=[preview,\@mmtarrowtipmonoleft-\@mmtarrowtippartialleft]
+\tikzstyle{adoption}=[preview,thin,double,-\@mmtarrowtip]
+% biviews: regular, partial, and left variants
+\tikzstyle{biview}=[preview,\@mmtarrowtip-\@mmtarrowtip]
+\tikzstyle{pbiview}=[preview,\@mmtreversearrowtippartial-\@mmtarrowtippartial]
+\tikzstyle{pbiviewleft}=[preview,\@mmtreversearrowtippartialleft-\@mmtarrowtippartialleft]
+% defining views (experimental)
+\tikzstyle{defview}=[preview,densely dotted,-\@mmtarrowtip]
+% meta-theory inclusion
+\tikzstyle{meta}=[dotted,-\@mmtarrowtip,thick]
+% conservative extensions (abbreviation)
+\tikzstyle{conservative}=[hooks-\@mmtarrowtip,double]
+% conservative development
+\tikzstyle{conservdev}=[hooks-\@mmtarrowtip,dashed,double]
+
+% antimorphisms as striktthroughs
+\tikzset{anti/.style={
+ decoration={markings, mark=between positions 0.2 and 0.8 step 4mm with {
+ \draw [thick,-] ++ (-3pt,-3pt) -- (3pt,3pt);}},
+ postaction={decorate}}}
+
+% parallel markup
+\tikzstyle{parallel}=[\@mmtarrowtip-\@mmtarrowtip,dashed]
+
+%%%% 3. Realms
+\tikzstyle{prerealm}=[draw=blue!40,rectangle,rounded corners,inner sep=10pt,inner ysep=20pt]
+\tikzstyle{realm}=[prerealm,fill=gray!4]
+\tikzstyle{pillar}=[prerealm,fill=gray!10]
+
+%%% 4. convenience macros
+%%% 4.1 the \mmtthy macro takes three arguments, name, decl, axioms and makes a
+% table-like structure
+\newcommand\mmtthy[3]{\def\@second{#2}\def\@third{#3}%
+\begin{array}{l}\textsf{#1}%
+\ifx\@second\@empty\else\\\hline #2\fi%
+\ifx\@third\@empty\else\\\hline #3\fi%
+\end{array}}
+%%% 4.2 the \mmtar takes two arguments, some tikz options, and an arrow style. \nmmtar
+% is a variant that also has a name on top.
+\newcommand\mmtar[2][]{\raisebox{.5ex}{\tikz[#1]{\draw[#2] (0,0) -- (.6,0);}}}
+\newcommand\nmmtar[3][]{\raisebox{.4ex}{\tikz[#1]{\draw[#2] (0,0) --
+ node[above]{\ensuremath{\scriptstyle #3}} (.8,0);}}}
+%%%% 3.3 Pushout symbols
+%% (after http://tex.stackexchange.com/questions/1144/pushouts-and-pullbacks)
+%% \nepushout[<pos>]{<basenode>}{<targetnode>} positions a pushout symbol
+%% (available separately as \pushoutsymb) <pos> of the way between <basenode>
+%% and <targetnode>.
+\usetikzlibrary{calc}
+\newcommand\@pushout[4][]{\def\@test{#1}%
+\ifx\@test\@empty\def\@@num{.5}\else\def\@@num{#1}\fi%
+\begin{scope}[shift=($(#2)!\@@num!(#3)$)]\@nameuse{@#4pushoutsymb}\end{scope}}
+\newcommand\@nepushoutsymb{\draw +(-.2,0) -- +(0,0) -- +(0,-.2);\fill +(-.1,-.1) circle (.03);}
+\newcommand\nepushoutsymb{\tikz{\@nepushoutsymb}}
+\newcommand\nepushout[3][]{\@pushout[#1]{#2}{#3}{ne}}
+
+\newcommand\@sepushoutsymb{\draw +(-.2,0) -- +(0,0) -- +(0,.2);\fill +(-.1,.1) circle (.03);}
+\newcommand\sepushoutsymb{\tikz{\@sepushoutsymb}}
+\newcommand\sepushout[3][]{\@pushout[#1]{#2}{#3}{se}}
+
+\newcommand\@nwpushoutsymb{\draw +(.2,0) -- +(0,0) -- +(0,-.2);\fill +(.1,-.1) circle (.03);}
+\newcommand\nwpushoutsymb{\tikz{\@nwpushoutsymb}}
+\newcommand\nwpushout[3][]{\@pushout[#1]{#2}{#3}{nw}}
+
+\newcommand\@swpushoutsymb{\draw +(.2,0) -- +(0,0) -- +(0,.2);\fill +(.1,.1) circle (.03);}
+\newcommand\swpushoutsymb{\tikz{\@swpushoutsymb}}
+\newcommand\swpushout[3][]{\@pushout[#1]{#2}{#3}{sw}}
+
+\newcommand\@npushoutsymb{\draw +(-.1,-.1) -- +(0,0) -- +(.1,-.1);\fill +(0,-.1) circle (.03);}
+\newcommand\npushoutsymb{\tikz{\@npushoutsymb}}
+\newcommand\npushout[3][]{\@pushout[#1]{#2}{#3}{n}}
+
+\newcommand\@spushoutsymb{\draw +(-.1,.1) -- +(0,0) -- +(.1,.1);\fill +(0,.1) circle (.03);}
+\newcommand\spushoutsymb{\tikz{\@spushoutsymb}}
+\newcommand\spushout[3][]{\@pushout[#1]{#2}{#3}{s}}
+
+\newcommand\@wpushoutsymb{\draw +(-.1,-.1) -- +(0,0) -- +(-.1,.1);\fill +(-.1,0) circle (.03);}
+\newcommand\wpushoutsymb{\tikz{\@wpushoutsymb}}
+\newcommand\wpushout[3][]{\@pushout[#1]{#2}{#3}{w}}
+
+\newcommand\@epushoutsymb{\draw +(.1,.1) -- +(0,0) -- +(.1,-.1);\fill +(.1,0) circle (.03);}
+\newcommand\epushoutsymb{\tikz{\@epushoutsymb}}
+\newcommand\epushout[3][]{\@pushout[#1]{#2}{#3}{e}}
+
+%%%%%% testing them:
+% \begin{tikzpicture}[scale=1.5]
+% \node (a) at (0,0) {a};
+% \node (b) at (1,0) {b};
+% \node (c) at (1,1) {c};
+% \node (d) at (0,1) {d};
+% \nepushout[.8]{a}c;
+% \nwpushout[.8]{b}d;
+% \sepushout[.8]{d}b;
+% \swpushout[.8]{c}a;
+% \draw (a) -- (b) -- (c) -- (d) -- (a);
+% \node (aa) at (4,0) {a};
+% \node (bb) at (3.5,.5) {b};
+% \node (cc) at (4,1) {c};
+% \node (dd) at (4.5,.5) {d};
+% \draw (aa) -- (bb) -- (cc) -- (dd) -- (aa);
+% \npushout[.8]{aa}{cc};
+% \spushout[.8]{cc}{aa};
+% \wpushout[.8]{bb}{dd};
+% \epushout[.8]{dd}{bb};
+% \end{tikzpicture}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "test"
+%%% End:
diff --git a/tikzlibrarydocicon.code.tex b/tikzlibrarydocicon.code.tex
new file mode 100755
index 0000000000000000000000000000000000000000..172e7a03576a1d62da75389f90baa6b6f378ec0e
--- /dev/null
+++ b/tikzlibrarydocicon.code.tex
@@ -0,0 +1 @@
+\input{pgflibrarytikzdocicon.code.tex}
diff --git a/tikzlibrarymmt.code.tex b/tikzlibrarymmt.code.tex
new file mode 100755
index 0000000000000000000000000000000000000000..834c6c31f1a00bb82dff986170219c5365a913fd
--- /dev/null
+++ b/tikzlibrarymmt.code.tex
@@ -0,0 +1 @@
+\input{pgflibrarytikzmmt.code.tex}
diff --git a/user.png b/user.png
new file mode 100644
index 0000000000000000000000000000000000000000..3a45e875f00b86627d80dced1df59f5b9d3999ba
Binary files /dev/null and b/user.png differ
diff --git a/wasysym.sty.ltxml b/wasysym.sty.ltxml
new file mode 100755
index 0000000000000000000000000000000000000000..324cf3542eb050bc814cf394af3917648fe2e3ff
--- /dev/null
+++ b/wasysym.sty.ltxml
@@ -0,0 +1,20 @@
+# -*- CPERL -*-
+# /=======================================================\ #
+# | wasysym.sty - Implementation for LaTeXML | #
+# | | #
+# |=======================================================| #
+# | Part of LaTeXML : http://dlmf.nist.gov/LaTeXML/ | #
+# | Copyright (c) 2006 arXMLiv group | #
+# | Released under the GNU Public License | #
+# \=======================================================/ #
+
+package LaTeXML::Package::Pool;
+use strict;
+use LaTeXML::Package;
+
+DefMacro('\cent', UTF(0xA2));
+DefMacro('\Join', "\x{2A1D}");
+DefMacro('\lightning',"\x{21AF}");
+DefMacro('\smiley',"\x{263A}");
+#**********************************************************************
+1;