src/HOL/UNITY/Comp/Progress.thy
changeset 58889 5b7a9633cfa8
parent 46577 e5438c5797ae
child 63146 f1ecba0272f9
equal deleted inserted replaced
58888:9537bf1c4853 58889:5b7a9633cfa8
     3     Copyright   2003  University of Cambridge
     3     Copyright   2003  University of Cambridge
     4 
     4 
     5 David Meier's thesis
     5 David Meier's thesis
     6 *)
     6 *)
     7 
     7 
     8 header{*Progress Set Examples*}
     8 section{*Progress Set Examples*}
     9 
     9 
    10 theory Progress imports "../UNITY_Main" begin
    10 theory Progress imports "../UNITY_Main" begin
    11 
    11 
    12 subsection {*The Composition of Two Single-Assignment Programs*}
    12 subsection {*The Composition of Two Single-Assignment Programs*}
    13 text{*Thesis Section 4.4.2*}
    13 text{*Thesis Section 4.4.2*}