%% -------------------------------------------------------------------------
%% Logical symbols
%% $Id: lsymbols.sty 3846 2016-11-10 08:52:47Z br $
%% -------------------------------------------------------------------------
%%
%% Copyright (C) 2016 by Burkhardt Renz
%% 
%% This file may be distributed and/or modified under the conditions
%% of the LaTeX Project Public License, either version 1.2 of this
%% license or (at your option) any later version.  The latest version
%% of this license is in:
%% 
%%    http://www.latex-project.org/lppl.txt
%% 
%% and version 1.2 or later is part of all distributions of LaTeX
%% version 1999/12/01 or later.
%% 
\NeedsTeXFormat{LaTeX2e}[1994/06/01]
\ProvidesPackage{lsymbols}[2016/04/01 Rev 1.0 Logical symbols Package]

\RequirePackage{MnSymbol}

%% general

\newcommand{\mequiv}{\Leftrightarrow}  % meta equivalence
\newcommand{\mimpl}{\Rightarrow}       % meta implication
\newcommand{\minvimpl}{\Leftarrow}     % meta inverse implication

\newcommand{\true}{\mathtt{T}}
\newcommand{\false}{\mathtt{F}}

% \lsem     from MnSymbol
% \rsem     from MnSymbol

% \models   from MnSymbol
\newcommand{\proves}{\vdash}
% \nmodels   from MnSymbol
\newcommand{\nproves}{\nvdash}

%% propositional logic

% \lnot from MnSymbol
% \land from MnSymbol
% \lor  from MnSymbol
\newcommand{\limpl}{\to}
\newcommand{\lequiv}{\leftrightarrow}
\newcommand{\verum}{\top}
\newcommand{\falsum}{\bot}

% \equiv from MnSymbol

%% predicate logic

% \forall  from MnSymbol
% \exists  from MnSymbol

%% linear temporal logic
\newcommand{\lnext}{\medcircle\,}
\newcommand{\luntil}{\mathcal{\:U\:}}
\newcommand{\lwuntil}{\mathcal{\:W\:}}
\newcommand{\lrelease}{\mathcal{\:R\:}}
\newcommand{\leventually}{\lozenge\,}
\newcommand{\lalways}{\medsquare\,}

\endinput
