Changeset 647 for Deliverables/D1.1


Ignore:
Timestamp:
Mar 7, 2011, 7:00:01 PM (9 years ago)
Author:
campbell
Message:

Minor WP3 edits.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D1.1/Presentations/WP3-brian.tex

    r637 r647  
    1010\lstdefinelanguage{coq}
    1111  {keywords={Definition,Lemma,Theorem,Remark,Qed,Save,Inductive,Record},
    12    morekeywords={[2]if,then,else},
     12   morekeywords={[2]if,then,else,forall,Prop},
    1313  }
    1414
    1515\lstdefinelanguage{matita}
    16   {keywords={ndefinition,nlemma,ntheorem,nremark,ninductive,nrecord,nqed,nlet,rec,match,with,Type,and,on},
    17    morekeywords={[2]nwhd,nnormalize,nelim,ncases,ndestruct},
     16  {keywords={ndefinition,nlemma,ntheorem,nremark,ninductive,nrecord,nqed,nlet,rec,match,with,and,on,return},
     17   morekeywords={[2]nwhd,nnormalize,nelim,ncases,ndestruct,Prop,Type},
    1818   mathescape=true,
    1919  }
     
    8282\colorbox{lightgreen}{New code.}
    8383\begin{itemize}
    84 \item Proven equivalent to the inductive semantics
     84\item Proved equivalent to the inductive semantics
    8585\end{itemize}
    8686\end{frame}
     
    323323  \begin{itemize}
    324324  \item[$\triangleright$] proof terms get in the way later on
     325  \item[$\triangleright$] providing separate theorems easier
    325326  \end{itemize}
    326 \item Full executions tricker --- final result requires ability to
     327\item Full executions trickier --- final result requires ability to
    327328      commit to (non-)termination
    328329  \begin{itemize}
Note: See TracChangeset for help on using the changeset viewer.