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/HoareParallel/OG_Hoare.thy
changeset 14398 c5c47703f763
parent 13601 fd3e3d6b37b2
child 15102 04b0e943fcc9
equal deleted inserted replaced
14397:b3b15305a1c9 14398:c5c47703f763 
   235  apply auto
 
   235  apply auto
 
   236  apply(rule AnnSeq)
 
   236  apply(rule AnnSeq)
 
   237   apply simp
 
   237   apply simp
 
   238  apply(rule AnnWhile)
 
   238  apply(rule AnnWhile)
 
   239   apply simp_all
 
   239   apply simp_all
 
   240  apply(fast)
 
       
   241 --{* Await *}
 
   240 --{* Await *}
 
   242 apply(frule ann_hoare_case_analysis,simp)
 
   241 apply(frule ann_hoare_case_analysis,simp)
 
   243 apply clarify
 
   242 apply clarify
 
   244 apply(drule atom_hoare_sound)
 
   243 apply(drule atom_hoare_sound)
 
   245  apply simp 
   244  apply simp
isabelle