src/HOL/IMP/Transition.ML
changeset 5278 a903b66822e2
parent 5223 4cb05273f764
child 6141 a6922171b396
     1.1 --- a/src/HOL/IMP/Transition.ML	Thu Aug 06 15:47:26 1998 +0200
     1.2 +++ b/src/HOL/IMP/Transition.ML	Thu Aug 06 15:48:13 1998 +0200
     1.3 @@ -27,8 +27,7 @@
     1.4  val hlemma = result();
     1.5  
     1.6  
     1.7 -Goal
     1.8 -  "!s t u c d. (c,s) -n-> (SKIP,t) --> (d,t) -*-> (SKIP,u) --> \
     1.9 +Goal "!s t u c d. (c,s) -n-> (SKIP,t) --> (d,t) -*-> (SKIP,u) --> \
    1.10  \              (c;d, s) -*-> (SKIP, u)";
    1.11  by (induct_tac "n" 1);
    1.12   by (fast_tac (claset() addIs [rtrancl_into_rtrancl2])1);
    1.13 @@ -60,8 +59,7 @@
    1.14  qed "evalc_impl_evalc1";
    1.15  
    1.16  
    1.17 -Goal
    1.18 -  "!c d s u. (c;d,s) -n-> (SKIP,u) --> \
    1.19 +Goal "!c d s u. (c;d,s) -n-> (SKIP,u) --> \
    1.20  \            (? t m. (c,s) -*-> (SKIP,t) & (d,t) -m-> (SKIP,u) & m <= n)";
    1.21  by (induct_tac "n" 1);
    1.22   (* case n = 0 *)
    1.23 @@ -117,8 +115,7 @@
    1.24  
    1.25  section "A Proof Without -n->";
    1.26  
    1.27 -Goal
    1.28 - "(c1,s1) -*-> (SKIP,s2) ==> \
    1.29 +Goal "(c1,s1) -*-> (SKIP,s2) ==> \
    1.30  \ (c2,s2) -*-> cs3 --> (c1;c2,s1) -*-> cs3";
    1.31  by (etac converse_rtrancl_induct2 1);
    1.32  by (fast_tac (claset() addIs [rtrancl_into_rtrancl2]) 1);
    1.33 @@ -183,8 +180,7 @@
    1.34  *)
    1.35  
    1.36  (*Delsimps [update_apply];*)
    1.37 -Goal 
    1.38 -  "((c,s) -1-> (c',s')) ==> (!t. <c',s'> -c-> t --> <c,s> -c-> t)";
    1.39 +Goal "((c,s) -1-> (c',s')) ==> (!t. <c',s'> -c-> t --> <c,s> -c-> t)";
    1.40  by (etac evalc1.induct 1);
    1.41  by Auto_tac;
    1.42  qed_spec_mp "FB_lemma3";