renamed the underlying relation of leadsTo from "leadsto"
to "leads" to reduce the risk of confusion

--- a/src/HOL/UNITY/WFair.ML	Tue Jun 08 10:30:04 1999 +0200
+++ b/src/HOL/UNITY/WFair.ML	Tue Jun 08 10:59:02 1999 +0200
@@ -75,12 +75,12 @@
 (*** leadsTo ***)
 
 Goalw [leadsTo_def] "F : A ensures B ==> F : A leadsTo B";
-by (blast_tac (claset() addIs [leadsto.Basis]) 1);
+by (blast_tac (claset() addIs [leads.Basis]) 1);
 qed "leadsTo_Basis";
 
 Goalw [leadsTo_def]
      "[| F : A leadsTo B;  F : B leadsTo C |] ==> F : A leadsTo C";
-by (blast_tac (claset() addIs [leadsto.Trans]) 1);
+by (blast_tac (claset() addIs [leads.Trans]) 1);
 qed "leadsTo_Trans";
 
 Goal "F : transient A ==> F : A leadsTo (-A)";
@@ -105,14 +105,14 @@
 (*The Union introduction rule as we should have liked to state it*)
 val prems = Goalw [leadsTo_def]
     "(!!A. A : S ==> F : A leadsTo B) ==> F : (Union S) leadsTo B";
-by (blast_tac (claset() addIs [leadsto.Union] addDs prems) 1);
+by (blast_tac (claset() addIs [leads.Union] addDs prems) 1);
 qed "leadsTo_Union";
 
 val prems = Goalw [leadsTo_def]
     "(!!A. A : S ==> F : (A Int C) leadsTo B) \
 \    ==> F : (Union S Int C) leadsTo B";
 by (simp_tac (HOL_ss addsimps [Int_Union_Union]) 1);
-by (blast_tac (claset() addIs [leadsto.Union] addDs prems) 1);
+by (blast_tac (claset() addIs [leads.Union] addDs prems) 1);
 qed "leadsTo_Union_Int";
 
 val prems = Goal
@@ -142,7 +142,7 @@
 \              ==> P A C; \
 \     !!B S. ALL A:S. F : A leadsTo B & P A B ==> P (Union S) B \
 \  |] ==> P za zb";
-by (rtac (major RS CollectD RS leadsto.induct) 1);
+by (rtac (major RS CollectD RS leads.induct) 1);
 by (REPEAT (blast_tac (claset() addIs prems) 1));
 qed "leadsTo_induct";
 

--- a/src/HOL/UNITY/WFair.thy	Tue Jun 08 10:30:04 1999 +0200
+++ b/src/HOL/UNITY/WFair.thy	Tue Jun 08 10:59:02 1999 +0200
@@ -23,24 +23,23 @@
   ensures :: "['a set, 'a set] => 'a program set"       (infixl 60)
 
   (*LEADS-TO constant for the inductive definition*)
-  leadsto :: "'a program => ('a set * 'a set) set"
+  leads :: "'a program => ('a set * 'a set) set"
 
   (*visible version of the LEADS-TO relation*)
   leadsTo :: "['a set, 'a set] => 'a program set"       (infixl 60)
 
-  
-inductive "leadsto F"
+
+inductive "leads F"
   intrs 
 
-    Basis  "F : A ensures B ==> (A,B) : leadsto F"
+    Basis  "F : A ensures B ==> (A,B) : leads F"
 
-    Trans  "[| (A,B) : leadsto F;  (B,C) : leadsto F |]
-	   ==> (A,C) : leadsto F"
+    Trans  "[| (A,B) : leads F;  (B,C) : leads F |] ==> (A,C) : leads F"
 
     (*Encoding using powerset of the desired axiom
-       (!!A. A : S ==> (A,B) : leadsto F) ==> (Union S, B) : leadsto F
+       (!!A. A : S ==> (A,B) : leads F) ==> (Union S, B) : leads F
     *)
-    Union  "(UN A:S. {(A,B)}) : Pow (leadsto F) ==> (Union S, B) : leadsto F"
+    Union  "(UN A:S. {(A,B)}) : Pow (leads F) ==> (Union S, B) : leads F"
 
   monos Pow_mono
 
@@ -49,7 +48,7 @@
 defs
   ensures_def "A ensures B == (A-B co A Un B) Int transient (A-B)"
 
-  leadsTo_def "A leadsTo B == {F. (A,B) : leadsto F}"
+  leadsTo_def "A leadsTo B == {F. (A,B) : leads F}"
 
 constdefs