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.
src/HOLCF/IOA/meta_theory/Traces.thy
changeset 12028 52aa183c15bb
parent 10835 f4745d77e620
child 12218 6597093b77e7
equal deleted inserted replaced
12027:1281e9bf57f6 12028:52aa183c15bb 
   123 
   123 
   124 (*  ------------------- Fair Traces ------------------------------ *)
 
   124 (*  ------------------- Fair Traces ------------------------------ *)
 
   125 
   125 
   126 laststate_def
 
   126 laststate_def
 
   127   "laststate ex == case Last$(snd ex) of
 
   127   "laststate ex == case Last$(snd ex) of
 
   128                       Undef  => fst ex
 
   128                       UU  => fst ex
 
   129                     | Def at => snd at"
 
   129                     | Def at => snd at"
 
   130 
   130 
   131 inf_often_def
 
   131 inf_often_def
 
   132   "inf_often P s == Infinite (Filter P$s)"
 
   132   "inf_often P s == Infinite (Filter P$s)"
 
   133 
   133
isabelle