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.
src/HOLCF/IOA/Modelcheck/MuIOA.thy
author wenzelm
Sat, 03 Sep 2005 16:50:22 +0200
changeset 17244 0b2ff9541727
parent 7299 743b22579a2f
child 22819 a7b425bb668c
permissions -rw-r--r--
converted to Isar theory format;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
7299
743b22579a2f quite a lot of tuning and cleanup;
wenzelm
parents: 6471
diff changeset 
     1
 







17244






0b2ff9541727
converted to Isar theory format;



wenzelm


parents: 
7299

diff
changeset




     2


(* $Id$ *)













0b2ff9541727
converted to Isar theory format;



wenzelm


parents: 
7299

diff
changeset




     3














0b2ff9541727
converted to Isar theory format;



wenzelm


parents: 
7299

diff
changeset




     4


theory MuIOA













0b2ff9541727
converted to Isar theory format;



wenzelm


parents: 
7299

diff
changeset




     5


imports IOA MuckeSyn













0b2ff9541727
converted to Isar theory format;



wenzelm


parents: 
7299

diff
changeset




     6


begin








6471






08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;



mueller


parents: 

diff
changeset




     7














08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;



mueller


parents: 

diff
changeset




     8


consts








17244






0b2ff9541727
converted to Isar theory format;



wenzelm


parents: 
7299

diff
changeset




     9


  Internal_of_A :: "'a => bool"













0b2ff9541727
converted to Isar theory format;



wenzelm


parents: 
7299

diff
changeset




    10


  Internal_of_C :: "'a => bool"













0b2ff9541727
converted to Isar theory format;



wenzelm


parents: 
7299

diff
changeset




    11


  Start_of_A :: "'a => bool"













0b2ff9541727
converted to Isar theory format;



wenzelm


parents: 
7299

diff
changeset




    12


  Start_of_C :: "'a => bool"













0b2ff9541727
converted to Isar theory format;



wenzelm


parents: 
7299

diff
changeset




    13


  Trans_of_A :: "'a => 'b => bool"













0b2ff9541727
converted to Isar theory format;



wenzelm


parents: 
7299

diff
changeset




    14


  Trans_of_C :: "'a => 'b => bool"













0b2ff9541727
converted to Isar theory format;



wenzelm


parents: 
7299

diff
changeset




    15


  IntStep_of_A :: "'a => bool"













0b2ff9541727
converted to Isar theory format;



wenzelm


parents: 
7299

diff
changeset




    16


  IntStepStar_of_A :: "'a => bool"













0b2ff9541727
converted to Isar theory format;



wenzelm


parents: 
7299

diff
changeset




    17


  Move_of_A :: "'a => 'b => bool"













0b2ff9541727
converted to Isar theory format;



wenzelm


parents: 
7299

diff
changeset




    18


  isSimCA :: "'a => bool"








6471






08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;



mueller


parents: 

diff
changeset




    19














08d12ef5fc19
added translation from IOA to mucalculus and corresponding modelchecker examples;



mueller


parents: 

diff
changeset




    20


end















isabelle