src/HOL/Imperative_HOL/Overview.thy
changeset 40671 5e46057ba8e0
parent 40358 b6ed3364753d
child 41413 64cd30d6b0b8
     1.1 --- a/src/HOL/Imperative_HOL/Overview.thy	Mon Nov 22 09:19:34 2010 +0100
     1.2 +++ b/src/HOL/Imperative_HOL/Overview.thy	Mon Nov 22 09:37:39 2010 +0100
     1.3 @@ -96,13 +96,13 @@
     1.4    To establish correctness of imperative programs, predicate
     1.5  
     1.6    \begin{quote}
     1.7 -    @{term_type crel}
     1.8 +    @{term_type effect}
     1.9    \end{quote}
    1.10  
    1.11    provides a simple relational calculus.  Primitive rules are @{text
    1.12 -  crelI} and @{text crelE}, rules appropriate for reasoning about
    1.13 -  imperative operations are available in the @{text crel_intros} and
    1.14 -  @{text crel_elims} fact collections.
    1.15 +  effectI} and @{text effectE}, rules appropriate for reasoning about
    1.16 +  imperative operations are available in the @{text effect_intros} and
    1.17 +  @{text effect_elims} fact collections.
    1.18  
    1.19    Often non-failure of imperative computations does not depend
    1.20    on the heap at all;  reasoning then can be easier using predicate
    1.21 @@ -114,10 +114,10 @@
    1.22    Introduction rules for @{const success} are available in the
    1.23    @{text success_intro} fact collection.
    1.24  
    1.25 -  @{const execute}, @{const crel}, @{const success} and @{const bind}
    1.26 +  @{const execute}, @{const effect}, @{const success} and @{const bind}
    1.27    are related by rules @{text execute_bind_success}, @{text
    1.28 -  success_bind_executeI}, @{text success_bind_crelI}, @{text
    1.29 -  crel_bindI}, @{text crel_bindE} and @{text execute_bind_eq_SomeI}.
    1.30 +  success_bind_executeI}, @{text success_bind_effectI}, @{text
    1.31 +  effect_bindI}, @{text effect_bindE} and @{text execute_bind_eq_SomeI}.
    1.32  *}
    1.33  
    1.34  
    1.35 @@ -235,7 +235,7 @@
    1.36        
    1.37      \item Whether one should prefer equational reasoning (fact
    1.38        collection @{text execute_simps} or relational reasoning (fact
    1.39 -      collections @{text crel_intros} and @{text crel_elims}) depends
    1.40 +      collections @{text effect_intros} and @{text effect_elims}) depends
    1.41        on the problems to solve.  For complex expressions or
    1.42        expressions involving binders, the relation style usually is
    1.43        superior but requires more proof text.