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/HOL/HOLCF/IOA/ABP/Correctness.thy
changeset 62008 cbedaddc9351
parent 62002 f1599e98c4d0
child 62009 ecb5212d5885
equal deleted inserted replaced
62007:3f8b97ceedb2 62008:cbedaddc9351 
     3 *)
 
     3 *)
 
     4 
     4 
     5 section \<open>The main correctness proof: System_fin implements System\<close>
 
     5 section \<open>The main correctness proof: System_fin implements System\<close>
 
     6 
     6 
     7 theory Correctness
 
     7 theory Correctness
 
     8 imports "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Env Impl Impl_finite
 
     8 imports "~~/src/HOL/HOLCF/IOA/IOA" Env Impl Impl_finite
 
     9 begin
 
     9 begin
 
    10 
    10 
    11 ML_file "Check.ML"
 
    11 ML_file "Check.ML"
 
    12 
    12 
    13 primrec reduce :: "'a list => 'a list"
 
    13 primrec reduce :: "'a list => 'a list"
isabelle