# HG changeset patch
# User paulson
# Date 929003891 -7200
# Node ID 5b8912f7bb6959021abbcee6d87b36735d5b4801
# Parent  d5dfe040c183de04960faedde22c2752f5e95bfc
shortened Follows to Fols

diff -r d5dfe040c183 -r 5b8912f7bb69 src/HOL/UNITY/Follows.ML
--- a/src/HOL/UNITY/Follows.ML	Thu Jun 10 10:37:29 1999 +0200
+++ b/src/HOL/UNITY/Follows.ML	Thu Jun 10 10:38:11 1999 +0200
@@ -23,7 +23,7 @@
 by (ALLGOALS (blast_tac (claset() addIs [monoD, order_trans])));
 qed "mono_LeadsTo_o";
 
-Goalw [Follows_def] "mono h ==> f Follows g <= (h o f) Follows (h o g)";
+Goalw [Follows_def] "mono h ==> f Fols g <= (h o f) Fols (h o g)";
 by (Clarify_tac 1);
 by (asm_full_simp_tac
     (simpset() addsimps [impOfSubs mono_Increasing_o,
@@ -32,7 +32,7 @@
 qed "mono_Follows_o";
 
 Goalw [Follows_def]
-     "[| F : f Follows g;  F: g Follows h |] ==> F : f Follows h";
+     "[| F : f Fols g;  F: g Fols h |] ==> F : f Fols h";
 by (asm_full_simp_tac (simpset() addsimps [Always_eq_includes_reachable]) 1);
 by (blast_tac (claset() addIs [order_trans, LeadsTo_Trans]) 1);
 qed "Follows_trans";
@@ -92,8 +92,8 @@
 qed "Follows_Un_lemma";
 
 Goalw [Follows_def]
-    "[| F : f' Follows f;  F: g' Follows g |] \
-\    ==> F : (%s. (f' s) Un (g' s)) Follows (%s. (f s) Un (g s))";
+    "[| F : f' Fols f;  F: g' Fols g |] \
+\    ==> F : (%s. (f' s) Un (g' s)) Fols (%s. (f s) Un (g s))";
 by (asm_full_simp_tac (simpset() addsimps [Increasing_Un, Always_Un]) 1);
 by Auto_tac;
 by (rtac LeadsTo_Trans 1);
diff -r d5dfe040c183 -r 5b8912f7bb69 src/HOL/UNITY/Follows.thy
--- a/src/HOL/UNITY/Follows.thy	Thu Jun 10 10:37:29 1999 +0200
+++ b/src/HOL/UNITY/Follows.thy	Thu Jun 10 10:38:11 1999 +0200
@@ -11,10 +11,10 @@
 constdefs
 
   Follows :: "['a => 'b::{order}, 'a => 'b::{order}] => 'a program set"
-                 (infixl 65)
-   "f Follows g == Increasing g Int Increasing f Int
-                   Always {s. f s <= g s} Int
-                   (INT k. {s. k <= g s} LeadsTo {s. k <= f s})"
+                 (infixl "Fols" 65)
+   "f Fols g == Increasing g Int Increasing f Int
+                Always {s. f s <= g s} Int
+                (INT k. {s. k <= g s} LeadsTo {s. k <= f s})"
 
 
 end