lstlangmizar.sty

%%
%% Mizar definition (c) 2012 Josef Urban
%%                           <Josef.Urban@gmail.com>
%%
%% minor enhancements (c) 2013 Christoph Lange
%%                             <math.semantic.web@gmail.com>
%%
\lstdefinelanguage{Mizar}%
{morekeywords={schemes,constructors,definitions,theorems,vocabularies,requirements,registrations,
notations,theorem,scheme,definition,registration,notation,axiom,proof,now,end,hereby,case,suppose,
for,ex,not,&,or,implies,iff,st,holds,being,does,assume,cases,given,hence,let,per,take,thus,and,
antonym,attr,as,be,begin,canceled,cluster,coherence,compatibility,consider,consistency,
contradiction,correctness,def,deffunc,defpred,environ,equals,existence,func,if,identify,
irreflexivity,it,means,mode,of,otherwise,over,pred,provided,qua,reconsider,redefine,reduce,
reducibility,reflexivity,reserve,struct,such,synonym,that,then,thesis,when,where,withis,
associativity,commutativity,connectedness,irreflexivity,reduce,reducibility,reflexivity,symmetry,
sethood,uniqueness,transitivity,idempotence,asymmetry,projectivity,involutiveness
	},% 
   sensitive, %
   morecomment=[l]{::},%
   morecomment=[n]{(:}{:)},%
   morestring=[d]",%
   literate={=>}{{$\Rightarrow$}}1 {>->}{{$\rightarrowtail$}}2{->}{{$\to$}}1
   {\/\\}{{$\wedge$}}1
   {|-}{{$\vdash$}}1
   {\\\/}{{$\vee$}}1
   {~}{{$\sim$}}1
   {<>}{{$\neq$}}1 %indeed... no.
  }[keywords,comments,strings]%