src/HOL/UNITY/Simple/Reachability.ML
changeset 11467 1064effe37f6
parent 11195 65ede8dfe304
child 11701 3d51fbf81c17
     1.1 --- a/src/HOL/UNITY/Simple/Reachability.ML	Mon Aug 06 15:54:29 2001 +0200
     1.2 +++ b/src/HOL/UNITY/Simple/Reachability.ML	Mon Aug 06 16:43:40 2001 +0200
     1.3 @@ -162,7 +162,7 @@
     1.4  
     1.5  
     1.6  Goalw [nmsg_gte_def, nmsg_lte_def,nmsg_gt_def, nmsg_eq_def]
     1.7 -     "((nmsg_gte 0 (v,w) Int nmsg_lte 1 (v,w)) Int (- nmsg_gt 0 (v,w) Un A)) \
     1.8 +     "((nmsg_gte 0 (v,w) Int nmsg_lte 1' (v,w)) Int (- nmsg_gt 0 (v,w) Un A)) \
     1.9  \     <= A Un nmsg_eq 0 (v,w)";
    1.10  by Auto_tac;
    1.11  qed "lemma4";
    1.12 @@ -170,7 +170,7 @@
    1.13  
    1.14  Goalw [nmsg_gte_def,nmsg_lte_def,nmsg_gt_def, nmsg_eq_def]
    1.15       "reachable v Int nmsg_eq 0 (v,w) = \
    1.16 -\     ((nmsg_gte 0 (v,w) Int nmsg_lte 1 (v,w)) Int \
    1.17 +\     ((nmsg_gte 0 (v,w) Int nmsg_lte 1' (v,w)) Int \
    1.18  \      (reachable v Int nmsg_lte 0 (v,w)))";
    1.19  by Auto_tac;
    1.20  qed "lemma5";