shortened Follows to Fols
authorpaulson
Thu Jun 10 10:38:11 1999 +0200 (1999-06-10)
changeset 68095b8912f7bb69
parent 6808 d5dfe040c183
child 6810 731c848f6f0c
shortened Follows to Fols
src/HOL/UNITY/Follows.ML
src/HOL/UNITY/Follows.thy
     1.1 --- a/src/HOL/UNITY/Follows.ML	Thu Jun 10 10:37:29 1999 +0200
     1.2 +++ b/src/HOL/UNITY/Follows.ML	Thu Jun 10 10:38:11 1999 +0200
     1.3 @@ -23,7 +23,7 @@
     1.4  by (ALLGOALS (blast_tac (claset() addIs [monoD, order_trans])));
     1.5  qed "mono_LeadsTo_o";
     1.6  
     1.7 -Goalw [Follows_def] "mono h ==> f Follows g <= (h o f) Follows (h o g)";
     1.8 +Goalw [Follows_def] "mono h ==> f Fols g <= (h o f) Fols (h o g)";
     1.9  by (Clarify_tac 1);
    1.10  by (asm_full_simp_tac
    1.11      (simpset() addsimps [impOfSubs mono_Increasing_o,
    1.12 @@ -32,7 +32,7 @@
    1.13  qed "mono_Follows_o";
    1.14  
    1.15  Goalw [Follows_def]
    1.16 -     "[| F : f Follows g;  F: g Follows h |] ==> F : f Follows h";
    1.17 +     "[| F : f Fols g;  F: g Fols h |] ==> F : f Fols h";
    1.18  by (asm_full_simp_tac (simpset() addsimps [Always_eq_includes_reachable]) 1);
    1.19  by (blast_tac (claset() addIs [order_trans, LeadsTo_Trans]) 1);
    1.20  qed "Follows_trans";
    1.21 @@ -92,8 +92,8 @@
    1.22  qed "Follows_Un_lemma";
    1.23  
    1.24  Goalw [Follows_def]
    1.25 -    "[| F : f' Follows f;  F: g' Follows g |] \
    1.26 -\    ==> F : (%s. (f' s) Un (g' s)) Follows (%s. (f s) Un (g s))";
    1.27 +    "[| F : f' Fols f;  F: g' Fols g |] \
    1.28 +\    ==> F : (%s. (f' s) Un (g' s)) Fols (%s. (f s) Un (g s))";
    1.29  by (asm_full_simp_tac (simpset() addsimps [Increasing_Un, Always_Un]) 1);
    1.30  by Auto_tac;
    1.31  by (rtac LeadsTo_Trans 1);
     2.1 --- a/src/HOL/UNITY/Follows.thy	Thu Jun 10 10:37:29 1999 +0200
     2.2 +++ b/src/HOL/UNITY/Follows.thy	Thu Jun 10 10:38:11 1999 +0200
     2.3 @@ -11,10 +11,10 @@
     2.4  constdefs
     2.5  
     2.6    Follows :: "['a => 'b::{order}, 'a => 'b::{order}] => 'a program set"
     2.7 -                 (infixl 65)
     2.8 -   "f Follows g == Increasing g Int Increasing f Int
     2.9 -                   Always {s. f s <= g s} Int
    2.10 -                   (INT k. {s. k <= g s} LeadsTo {s. k <= f s})"
    2.11 +                 (infixl "Fols" 65)
    2.12 +   "f Fols g == Increasing g Int Increasing f Int
    2.13 +                Always {s. f s <= g s} Int
    2.14 +                (INT k. {s. k <= g s} LeadsTo {s. k <= f s})"
    2.15  
    2.16  
    2.17  end