Mercurial Mercurial > repos > isabelle / comparison
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/PDL.thy
changeset 10122 194c7349b6c0
parent 9958 67f2920862c7
child 10133 e187dacd248f
equal deleted inserted replaced
10121:fb9be005cc44 10122:194c7349b6c0 
     1 theory PDL = Main:;
 
     1 (*<*)theory PDL = Base:(*>*)
 
     2 
     2 
     3 typedecl atom;
 
     3 subsection{*Propositional dynmic logic---PDL*}
 
     4 types state = "atom set";
 
       
     5 
     4 
     6 datatype ctl_form = Atom atom
 
     5 datatype ctl_form = Atom atom
 
     7                   | NOT ctl_form
 
     6                   | NOT ctl_form
 
     8                   | And ctl_form ctl_form
 
     7                   | And ctl_form ctl_form
 
     9                   | AX ctl_form
 
     8                   | AX ctl_form
isabelle