Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
doc-src/TutorialI/CTL/ctl.tex
author chaieb
Wed, 19 May 2004 11:23:59 +0200
changeset 14758 af3b71a46a1c
parent 11458 09a6c44a48ea
child 48522 708278fc2dff
permissions -rw-r--r--
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller. the tactic has also changed and allows the abstaction over fuction occurences whose type is nat or int.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
11458
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 10178
diff changeset 
     1
 
\index{model checking example|(}%
10178
aecb5bf6f76f *** empty log message ***
nipkow
parents: 10133
diff changeset 
     2
 
\index{lfp@{\texttt{lfp}}!applications of|see{CTL}}
10123
9469c039ff57 *** empty log message ***
nipkow
parents:
diff changeset 
     3
 
\input{CTL/document/Base.tex}
9469c039ff57 *** empty log message ***
nipkow
parents:
diff changeset 
     4
 
\input{CTL/document/PDL.tex}
10133
e187dacd248f *** empty log message ***
nipkow
parents: 10123
diff changeset 
     5
 
\input{CTL/document/CTL.tex}
11458
09a6c44a48ea numerous stylistic changes and indexing
paulson
parents: 10178
diff changeset 
     6
 
\index{model checking example|)}
isabelle