Added a few lemmas.
Renamed expand_const -> split_const.

--- a/src/HOL/Arith.ML	Mon Apr 27 13:47:46 1998 +0200
+++ b/src/HOL/Arith.ML	Mon Apr 27 16:45:11 1998 +0200
@@ -29,7 +29,7 @@
    However, none of the generalizations are currently in the simpset,
    and I dread to think what happens if I put them in *)
 goal thy "!!n. 0 < n ==> Suc(n-1) = n";
-by (asm_simp_tac (simpset() addsplits [expand_nat_case]) 1);
+by (asm_simp_tac (simpset() addsplits [split_nat_case]) 1);
 qed "Suc_pred";
 Addsimps [Suc_pred];
 
@@ -114,7 +114,7 @@
 goal thy "!!n. 0<n ==> m + (n-1) = (m+n)-1";
 by (exhaust_tac "m" 1);
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [diff_Suc]
-                                      addsplits [expand_nat_case])));
+                                      addsplits [split_nat_case])));
 qed "add_pred";
 Addsimps [add_pred];
 

--- a/src/HOL/Finite.ML	Mon Apr 27 13:47:46 1998 +0200
+++ b/src/HOL/Finite.ML	Mon Apr 27 16:45:11 1998 +0200
@@ -111,23 +111,23 @@
 AddIffs [finite_Diff_singleton];
 
 (*Lemma for proving finite_imageD*)
-goal Finite.thy "!!A. finite B ==> !A. f``A = B --> inj_onto f A --> finite A";
+goal Finite.thy "!!A. finite B ==> !A. f``A = B --> inj_on f A --> finite A";
 by (etac finite_induct 1);
  by (ALLGOALS Asm_simp_tac);
 by (Clarify_tac 1);
 by (subgoal_tac "EX y:A. f y = x & F = f``(A-{y})" 1);
  by (Clarify_tac 1);
- by (full_simp_tac (simpset() addsimps [inj_onto_def]) 1);
+ by (full_simp_tac (simpset() addsimps [inj_on_def]) 1);
  by (Blast_tac 1);
 by (thin_tac "ALL A. ?PP(A)" 1);
 by (forward_tac [[equalityD2, insertI1] MRS subsetD] 1);
 by (Clarify_tac 1);
 by (res_inst_tac [("x","xa")] bexI 1);
 by (ALLGOALS 
-    (asm_full_simp_tac (simpset() addsimps [inj_onto_image_set_diff])));
+    (asm_full_simp_tac (simpset() addsimps [inj_on_image_set_diff])));
 val lemma = result();
 
-goal Finite.thy "!!A. [| finite(f``A);  inj_onto f A |] ==> finite A";
+goal Finite.thy "!!A. [| finite(f``A);  inj_on f A |] ==> finite A";
 by (dtac lemma 1);
 by (Blast_tac 1);
 qed "finite_imageD";
@@ -156,7 +156,7 @@
 by (rtac finite_subset 2);
 by (assume_tac 3);
 by (ALLGOALS
-    (fast_tac (claset() addSDs [rewrite_rule [inj_onto_def] finite_imageD])));
+    (fast_tac (claset() addSDs [rewrite_rule [inj_on_def] finite_imageD])));
 val lemma = result();
 
 goal Finite.thy "finite(Pow A) = finite A";
@@ -174,8 +174,8 @@
 by (subgoal_tac "r^-1 = (%(x,y).(y,x))``r" 1);
  by (Asm_simp_tac 1);
  by (rtac iffI 1);
-  by (etac (rewrite_rule [inj_onto_def] finite_imageD) 1);
-  by (simp_tac (simpset() addsplits [expand_split]) 1);
+  by (etac (rewrite_rule [inj_on_def] finite_imageD) 1);
+  by (simp_tac (simpset() addsplits [split_split]) 1);
  by (etac finite_imageI 1);
 by (simp_tac (simpset() addsimps [converse_def,image_def]) 1);
 by Auto_tac;
@@ -370,11 +370,11 @@
 qed "card_insert";
 Addsimps [card_insert];
 
-goal Finite.thy "!!A. finite(A) ==> inj_onto f A --> card (f `` A) = card A";
+goal Finite.thy "!!A. finite(A) ==> inj_on f A --> card (f `` A) = card A";
 by (etac finite_induct 1);
 by (ALLGOALS Asm_simp_tac);
 by Safe_tac;
-by (rewtac inj_onto_def);
+by (rewtac inj_on_def);
 by (Blast_tac 1);
 by (stac card_insert_disjoint 1);
 by (etac finite_imageI 1);
@@ -387,9 +387,9 @@
 by (ALLGOALS (asm_simp_tac (simpset() addsimps [Pow_insert])));
 by (stac card_Un_disjoint 1);
 by (EVERY (map (blast_tac (claset() addIs [finite_imageI])) [3,2,1]));
-by (subgoal_tac "inj_onto (insert x) (Pow F)" 1);
+by (subgoal_tac "inj_on (insert x) (Pow F)" 1);
 by (asm_simp_tac (simpset() addsimps [card_image, Pow_insert]) 1);
-by (rewtac inj_onto_def);
+by (rewtac inj_on_def);
 by (blast_tac (claset() addSEs [equalityE]) 1);
 qed "card_Pow";
 Addsimps [card_Pow];

--- a/src/HOL/Fun.ML	Mon Apr 27 13:47:46 1998 +0200
+++ b/src/HOL/Fun.ML	Mon Apr 27 16:45:11 1998 +0200
@@ -77,52 +77,52 @@
 qed "inj_transfer";
 
 
-(*** inj_onto f A: f is one-to-one over A ***)
+(*** inj_on f A: f is one-to-one over A ***)
 
-val prems = goalw thy [inj_onto_def]
-    "(!! x y. [| f(x) = f(y);  x:A;  y:A |] ==> x=y) ==> inj_onto f A";
+val prems = goalw thy [inj_on_def]
+    "(!! x y. [| f(x) = f(y);  x:A;  y:A |] ==> x=y) ==> inj_on f A";
 by (blast_tac (claset() addIs prems) 1);
-qed "inj_ontoI";
+qed "inj_onI";
 
 val [major] = goal thy 
-    "(!!x. x:A ==> g(f(x)) = x) ==> inj_onto f A";
-by (rtac inj_ontoI 1);
+    "(!!x. x:A ==> g(f(x)) = x) ==> inj_on f A";
+by (rtac inj_onI 1);
 by (etac (apply_inverse RS trans) 1);
 by (REPEAT (eresolve_tac [asm_rl,major] 1));
-qed "inj_onto_inverseI";
+qed "inj_on_inverseI";
 
-val major::prems = goalw thy [inj_onto_def]
-    "[| inj_onto f A;  f(x)=f(y);  x:A;  y:A |] ==> x=y";
+val major::prems = goalw thy [inj_on_def]
+    "[| inj_on f A;  f(x)=f(y);  x:A;  y:A |] ==> x=y";
 by (rtac (major RS bspec RS bspec RS mp) 1);
 by (REPEAT (resolve_tac prems 1));
-qed "inj_ontoD";
+qed "inj_onD";
 
-goal thy "!!x y.[| inj_onto f A;  x:A;  y:A |] ==> (f(x)=f(y)) = (x=y)";
-by (blast_tac (claset() addSDs [inj_ontoD]) 1);
-qed "inj_onto_iff";
+goal thy "!!x y.[| inj_on f A;  x:A;  y:A |] ==> (f(x)=f(y)) = (x=y)";
+by (blast_tac (claset() addSDs [inj_onD]) 1);
+qed "inj_on_iff";
 
 val major::prems = goal thy
-    "[| inj_onto f A;  ~x=y;  x:A;  y:A |] ==> ~ f(x)=f(y)";
+    "[| inj_on f A;  ~x=y;  x:A;  y:A |] ==> ~ f(x)=f(y)";
 by (rtac contrapos 1);
-by (etac (major RS inj_ontoD) 2);
+by (etac (major RS inj_onD) 2);
 by (REPEAT (resolve_tac prems 1));
-qed "inj_onto_contraD";
+qed "inj_on_contraD";
 
-goalw thy [inj_onto_def]
-    "!!A B. [| A<=B; inj_onto f B |] ==> inj_onto f A";
+goalw thy [inj_on_def]
+    "!!A B. [| A<=B; inj_on f B |] ==> inj_on f A";
 by (Blast_tac 1);
-qed "subset_inj_onto";
+qed "subset_inj_on";
 
 
 (*** Lemmas about inj ***)
 
 goalw thy [o_def]
-    "!!f g. [| inj(f);  inj_onto g (range f) |] ==> inj(g o f)";
-by (fast_tac (claset() addIs [injI] addEs [injD, inj_ontoD]) 1);
+    "!!f g. [| inj(f);  inj_on g (range f) |] ==> inj(g o f)";
+by (fast_tac (claset() addIs [injI] addEs [injD, inj_onD]) 1);
 qed "comp_inj";
 
-val [prem] = goal thy "inj(f) ==> inj_onto f A";
-by (blast_tac (claset() addIs [prem RS injD, inj_ontoI]) 1);
+val [prem] = goal thy "inj(f) ==> inj_on f A";
+by (blast_tac (claset() addIs [prem RS injD, inj_onI]) 1);
 qed "inj_imp";
 
 val [prem] = goalw thy [inv_def] "y : range(f) ==> f(inv f y) = y";
@@ -135,20 +135,20 @@
 by (REPEAT (resolve_tac (prems @ [f_inv_f]) 1));
 qed "inv_injective";
 
-goal thy "!!f. [| inj(f);  A<=range(f) |] ==> inj_onto (inv f) A";
-by (fast_tac (claset() addIs [inj_ontoI] 
+goal thy "!!f. [| inj(f);  A<=range(f) |] ==> inj_on (inv f) A";
+by (fast_tac (claset() addIs [inj_onI] 
                       addEs [inv_injective,injD]) 1);
-qed "inj_onto_inv";
+qed "inj_on_inv";
 
-goalw thy [inj_onto_def]
-   "!!f. [| inj_onto f C;  A<=C;  B<=C |] ==> f``(A Int B) = f``A Int f``B";
+goalw thy [inj_on_def]
+   "!!f. [| inj_on f C;  A<=C;  B<=C |] ==> f``(A Int B) = f``A Int f``B";
 by (Blast_tac 1);
-qed "inj_onto_image_Int";
+qed "inj_on_image_Int";
 
-goalw thy [inj_onto_def]
-   "!!f. [| inj_onto f C;  A<=C;  B<=C |] ==> f``(A-B) = f``A - f``B";
+goalw thy [inj_on_def]
+   "!!f. [| inj_on f C;  A<=C;  B<=C |] ==> f``(A-B) = f``A - f``B";
 by (Blast_tac 1);
-qed "inj_onto_image_set_diff";
+qed "inj_on_image_set_diff";
 
 goalw thy [inj_def] "!!f. inj f ==> f``(A Int B) = f``A Int f``B";
 by (Blast_tac 1);

--- a/src/HOL/Fun.thy	Mon Apr 27 13:47:46 1998 +0200
+++ b/src/HOL/Fun.thy	Mon Apr 27 16:45:11 1998 +0200
@@ -12,15 +12,15 @@
                        (subset_refl,subset_trans,subset_antisym,psubset_eq)
 consts
 
-  inj, surj     :: ('a => 'b) => bool                   (*inj/surjective*)
-  inj_onto      :: ['a => 'b, 'a set] => bool
-  inv           :: ('a => 'b) => ('b => 'a)
+  inj, surj   :: ('a => 'b) => bool                   (*inj/surjective*)
+  inj_on      :: ['a => 'b, 'a set] => bool
+  inv         :: ('a => 'b) => ('b => 'a)
 
 defs
 
-  inj_def       "inj f          == ! x y. f(x)=f(y) --> x=y"
-  inj_onto_def  "inj_onto f A   == ! x:A. ! y:A. f(x)=f(y) --> x=y"
-  surj_def      "surj f         == ! y. ? x. y=f(x)"
-  inv_def       "inv(f::'a=>'b) == (% y. @x. f(x)=y)"
+  inj_def     "inj f          == ! x y. f(x)=f(y) --> x=y"
+  inj_on_def  "inj_on f A     == ! x:A. ! y:A. f(x)=f(y) --> x=y"
+  surj_def    "surj f         == ! y. ? x. y=f(x)"
+  inv_def     "inv(f::'a=>'b) == (% y. @x. f(x)=y)"
 
 end

--- a/src/HOL/IsaMakefile	Mon Apr 27 13:47:46 1998 +0200
+++ b/src/HOL/IsaMakefile	Mon Apr 27 16:45:11 1998 +0200
@@ -104,11 +104,15 @@
 
 HOL-Lex: HOL $(LOG)/HOL-Lex.gz
 
-$(LOG)/HOL-Lex.gz: $(OUT)/HOL Lex/Auto.thy Lex/Auto.ML \
+$(LOG)/HOL-Lex.gz: $(OUT)/HOL \
   Lex/AutoChopper.thy Lex/AutoChopper.ML Lex/AutoChopper1.thy \
-  Lex/Chopper.thy Lex/Prefix.thy Lex/Prefix.ML Lex/ROOT.ML \
-  Lex/Regset_of_auto.ML Lex/Regset_of_auto.thy Lex/MaxChop.thy Lex/MaxChop.ML \
-  Lex/MaxPrefix.thy Lex/MaxPrefix.ML Lex/AutoMaxChop.thy Lex/AutoMaxChop.ML
+  Lex/AutoMaxChop.thy Lex/AutoMaxChop.ML Lex/AutoProj.thy Lex/AutoProj.ML \
+  Lex/Automata.thy Lex/Automata.ML Lex/Chopper.thy Lex/DA.thy Lex/DA.ML \
+  Lex/MaxChop.thy Lex/MaxChop.ML Lex/MaxPrefix.thy Lex/MaxPrefix.ML \
+  Lex/NA.thy Lex/NAe.thy Lex/NAe.ML Lex/NAe_of_RegExp.thy Lex/NAe_of_RegExp.ML\
+  Lex/Prefix.thy Lex/Prefix.ML Lex/ROOT.ML \
+  Lex/RegExp.thy Lex/RegSet.thy Lex/RegSet.ML \
+  Lex/RegSet_of_nat_DA.thy Lex/RegSet_of_nat_DA.ML
 	@$(ISATOOL) usedir $(OUT)/HOL Lex
 
 

--- a/src/HOL/List.ML	Mon Apr 27 13:47:46 1998 +0200
+++ b/src/HOL/List.ML	Mon Apr 27 16:45:11 1998 +0200
@@ -19,6 +19,15 @@
 by (Asm_simp_tac 1);
 qed "neq_Nil_conv";
 
+(* Induction over the length of a list: *)
+val prems = goal thy
+ "(!!xs::'a list. (!ys. length ys < length xs --> P ys) ==> P xs) ==> P xs";
+by (res_inst_tac [("P","P"),("r","measure length::('a list * 'a list)set")]
+     wf_induct 1);
+by (Simp_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [measure_def,inv_image_def]) 1);
+by (eresolve_tac prems 1);
+qed "list_length_induct";
 
 (** "lists": the list-forming operator over sets **)
 
@@ -219,6 +228,40 @@
 qed "tl_append2";
 Addsimps [tl_append2];
 
+
+(** Snoc exhaustion and induction **)
+section "Snoc exhaustion and induction";
+
+goal thy "xs ~= [] --> (? ys y. xs = ys@[y])";
+by(induct_tac "xs" 1);
+by(Simp_tac 1);
+by(exhaust_tac "list" 1);
+ by(Asm_simp_tac 1);
+ by(res_inst_tac [("x","[]")] exI 1);
+ by(Simp_tac 1);
+by(Asm_full_simp_tac 1);
+by(Clarify_tac 1);
+by(res_inst_tac [("x","a#ys")] exI 1);
+by(Asm_simp_tac 1);
+val lemma = result();
+
+goal thy  "(xs = [] --> P) -->  (!ys y. xs = ys@[y] --> P) --> P";
+by(cut_facts_tac [lemma] 1);
+by(Blast_tac 1);
+bind_thm ("snoc_exhaust",
+  impI RSN (2,allI RSN (2,allI RSN (2,impI RS (result() RS mp RS mp)))));
+
+val prems = goal thy "[| P []; !!x xs. P xs ==> P(xs@[x]) |] ==> P xs";
+by(res_inst_tac [("xs","xs")] list_length_induct 1);
+by(res_inst_tac [("xs","xs")] snoc_exhaust 1);
+ by(Clarify_tac 1);
+ brs prems 1;
+by(Clarify_tac 1);
+brs prems 1;
+auto();
+qed "snoc_induct";
+
+
 (** map **)
 
 section "map";

--- a/src/HOL/NatDef.ML	Mon Apr 27 13:47:46 1998 +0200
+++ b/src/HOL/NatDef.ML	Mon Apr 27 16:45:11 1998 +0200
@@ -85,15 +85,15 @@
 by (rtac Rep_Nat_inverse 1);
 qed "inj_Rep_Nat";
 
-goal thy "inj_onto Abs_Nat Nat";
-by (rtac inj_onto_inverseI 1);
+goal thy "inj_on Abs_Nat Nat";
+by (rtac inj_on_inverseI 1);
 by (etac Abs_Nat_inverse 1);
-qed "inj_onto_Abs_Nat";
+qed "inj_on_Abs_Nat";
 
 (*** Distinctness of constructors ***)
 
 goalw thy [Zero_def,Suc_def] "Suc(m) ~= 0";
-by (rtac (inj_onto_Abs_Nat RS inj_onto_contraD) 1);
+by (rtac (inj_on_Abs_Nat RS inj_on_contraD) 1);
 by (rtac Suc_Rep_not_Zero_Rep 1);
 by (REPEAT (resolve_tac [Rep_Nat, Suc_RepI, Zero_RepI] 1));
 qed "Suc_not_Zero";
@@ -109,7 +109,7 @@
 
 goalw thy [Suc_def] "inj(Suc)";
 by (rtac injI 1);
-by (dtac (inj_onto_Abs_Nat RS inj_ontoD) 1);
+by (dtac (inj_on_Abs_Nat RS inj_onD) 1);
 by (REPEAT (resolve_tac [Rep_Nat, Suc_RepI] 1));
 by (dtac (inj_Suc_Rep RS injD) 1);
 by (etac (inj_Rep_Nat RS injD) 1);
@@ -483,7 +483,7 @@
   "m=n ==> nat_rec a f m = nat_rec a f n"
   (fn [prem] => [rtac (prem RS arg_cong) 1]);
 
-qed_goal "expand_nat_case" thy
+qed_goal "split_nat_case" thy
   "P(nat_case z s n) = ((n=0 --> P z) & (!m. n = Suc m --> P(s m)))"
   (fn _ => [nat_ind_tac "n" 1, ALLGOALS Asm_simp_tac]);
 

--- a/src/HOL/Prod.ML	Mon Apr 27 13:47:46 1998 +0200
+++ b/src/HOL/Prod.ML	Mon Apr 27 16:45:11 1998 +0200
@@ -19,14 +19,14 @@
             rtac conjI, rtac refl, rtac refl]);
 qed "Pair_Rep_inject";
 
-goal Prod.thy "inj_onto Abs_Prod Prod";
-by (rtac inj_onto_inverseI 1);
+goal Prod.thy "inj_on Abs_Prod Prod";
+by (rtac inj_on_inverseI 1);
 by (etac Abs_Prod_inverse 1);
-qed "inj_onto_Abs_Prod";
+qed "inj_on_Abs_Prod";
 
 val prems = goalw Prod.thy [Pair_def]
     "[| (a, b) = (a',b');  [| a=a';  b=b' |] ==> R |] ==> R";
-by (rtac (inj_onto_Abs_Prod RS inj_ontoD RS Pair_Rep_inject RS conjE) 1);
+by (rtac (inj_on_Abs_Prod RS inj_onD RS Pair_Rep_inject RS conjE) 1);
 by (REPEAT (ares_tac (prems@[ProdI]) 1));
 qed "Pair_inject";
 
@@ -150,16 +150,16 @@
 by (stac surjective_pairing 1);
 by (stac split 1);
 by (Blast_tac 1);
-qed "expand_split";
+qed "split_split";
 
 (* could be done after split_tac has been speeded up significantly:
-simpset_ref() := simpset() addsplits [expand_split];
+simpset_ref() := simpset() addsplits [split_split];
    precompute the constants involved and don't do anything unless
    the current goal contains one of those constants
 *)
 
 goal Prod.thy "R (split c p) = (~(? x y. p = (x,y) & (~R (c x y))))";
-by (stac expand_split 1);
+by (stac split_split 1);
 by (Simp_tac 1);
 qed "expand_split_asm";
 

--- a/src/HOL/Relation.ML	Mon Apr 27 13:47:46 1998 +0200
+++ b/src/HOL/Relation.ML	Mon Apr 27 16:45:11 1998 +0200
@@ -64,6 +64,10 @@
 
 Addsimps [R_O_id,id_O_R];
 
+goal thy "(R O S) O T = R O (S O T)";
+by (Blast_tac 1);
+qed "O_assoc";
+
 goal thy "!!r s. [| r'<=r; s'<=s |] ==> (r' O s') <= (r O s)";
 by (Blast_tac 1);
 qed "comp_mono";

--- a/src/HOL/Set.ML	Mon Apr 27 13:47:46 1998 +0200
+++ b/src/HOL/Set.ML	Mon Apr 27 16:45:11 1998 +0200
@@ -643,19 +643,19 @@
 
 
 (** Rewrite rules for boolean case-splitting: faster than 
-	addsplits[expand_if]
+	addsplits[split_if]
 **)
 
-bind_thm ("expand_if_eq1", read_instantiate [("P", "%x. x = ?b")] expand_if);
-bind_thm ("expand_if_eq2", read_instantiate [("P", "%x. ?a = x")] expand_if);
+bind_thm ("split_if_eq1", read_instantiate [("P", "%x. x = ?b")] split_if);
+bind_thm ("split_if_eq2", read_instantiate [("P", "%x. ?a = x")] split_if);
 
-bind_thm ("expand_if_mem1", 
-    read_instantiate_sg (sign_of Set.thy) [("P", "%x. x : ?b")] expand_if);
-bind_thm ("expand_if_mem2", 
-    read_instantiate_sg (sign_of Set.thy) [("P", "%x. ?a : x")] expand_if);
+bind_thm ("split_if_mem1", 
+    read_instantiate_sg (sign_of Set.thy) [("P", "%x. x : ?b")] split_if);
+bind_thm ("split_if_mem2", 
+    read_instantiate_sg (sign_of Set.thy) [("P", "%x. ?a : x")] split_if);
 
-val expand_ifs = [if_bool_eq_conj, expand_if_eq1, expand_if_eq2,
-		  expand_if_mem1, expand_if_mem2];
+val split_ifs = [if_bool_eq_conj, split_if_eq1, split_if_eq2,
+		  split_if_mem1, split_if_mem2];
 
 
 (*Each of these has ALREADY been added to simpset() above.*)

--- a/src/HOL/Sum.ML	Mon Apr 27 13:47:46 1998 +0200
+++ b/src/HOL/Sum.ML	Mon Apr 27 16:45:11 1998 +0200
@@ -19,10 +19,10 @@
 by (EVERY1 [rtac CollectI, rtac disjI2, rtac exI, rtac refl]);
 qed "Inr_RepI";
 
-goal Sum.thy "inj_onto Abs_Sum Sum";
-by (rtac inj_onto_inverseI 1);
+goal Sum.thy "inj_on Abs_Sum Sum";
+by (rtac inj_on_inverseI 1);
 by (etac Abs_Sum_inverse 1);
-qed "inj_onto_Abs_Sum";
+qed "inj_on_Abs_Sum";
 
 (** Distinctness of Inl and Inr **)
 
@@ -34,7 +34,7 @@
 qed "Inl_Rep_not_Inr_Rep";
 
 goalw Sum.thy [Inl_def,Inr_def] "Inl(a) ~= Inr(b)";
-by (rtac (inj_onto_Abs_Sum RS inj_onto_contraD) 1);
+by (rtac (inj_on_Abs_Sum RS inj_on_contraD) 1);
 by (rtac Inl_Rep_not_Inr_Rep 1);
 by (rtac Inl_RepI 1);
 by (rtac Inr_RepI 1);
@@ -63,7 +63,7 @@
 
 goalw Sum.thy [Inl_def] "inj(Inl)";
 by (rtac injI 1);
-by (etac (inj_onto_Abs_Sum RS inj_ontoD RS Inl_Rep_inject) 1);
+by (etac (inj_on_Abs_Sum RS inj_onD RS Inl_Rep_inject) 1);
 by (rtac Inl_RepI 1);
 by (rtac Inl_RepI 1);
 qed "inj_Inl";
@@ -71,7 +71,7 @@
 
 goalw Sum.thy [Inr_def] "inj(Inr)";
 by (rtac injI 1);
-by (etac (inj_onto_Abs_Sum RS inj_ontoD RS Inr_Rep_inject) 1);
+by (etac (inj_on_Abs_Sum RS inj_onD RS Inr_Rep_inject) 1);
 by (rtac Inr_RepI 1);
 by (rtac Inr_RepI 1);
 qed "inj_Inr";
@@ -150,7 +150,7 @@
 \             ((! x. s = Inl(x) --> R(f(x))) & (! y. s = Inr(y) --> R(g(y))))";
 by (res_inst_tac [("s","s")] sumE 1);
 by Auto_tac;
-qed "expand_sum_case";
+qed "split_sum_case";
 
 (*Prevents simplification of f and g: much faster*)
 qed_goal "sum_case_weak_cong" Sum.thy

--- a/src/HOL/Trancl.ML	Mon Apr 27 13:47:46 1998 +0200
+++ b/src/HOL/Trancl.ML	Mon Apr 27 16:45:11 1998 +0200
@@ -115,6 +115,13 @@
 qed "rtrancl_idemp";
 Addsimps [rtrancl_idemp];
 
+goal thy "R^* O R^* = R^*";
+br set_ext 1;
+by(split_all_tac 1);
+by(blast_tac (claset() addIs [rtrancl_trans]) 1);
+qed "rtrancl_idemp_self_comp";
+Addsimps [rtrancl_idemp_self_comp];
+
 goal Trancl.thy "!!r s. r <= s^* ==> r^* <= s^*";
 by (dtac rtrancl_mono 1);
 by (Asm_full_simp_tac 1);

--- a/src/HOL/Univ.ML	Mon Apr 27 13:47:46 1998 +0200
+++ b/src/HOL/Univ.ML	Mon Apr 27 16:45:11 1998 +0200
@@ -58,12 +58,12 @@
 by (rtac Rep_Node_inverse 1);
 qed "inj_Rep_Node";
 
-goal Univ.thy "inj_onto Abs_Node Node";
-by (rtac inj_onto_inverseI 1);
+goal Univ.thy "inj_on Abs_Node Node";
+by (rtac inj_on_inverseI 1);
 by (etac Abs_Node_inverse 1);
-qed "inj_onto_Abs_Node";
+qed "inj_on_Abs_Node";
 
-val Abs_Node_inject = inj_onto_Abs_Node RS inj_ontoD;
+val Abs_Node_inject = inj_on_Abs_Node RS inj_onD;
 
 
 (*** Introduction rules for Node ***)

--- a/src/HOL/simpdata.ML	Mon Apr 27 13:47:46 1998 +0200
+++ b/src/HOL/simpdata.ML	Mon Apr 27 16:45:11 1998 +0200
@@ -209,7 +209,7 @@
 prove "disj_not1" "(~P | Q) = (P --> Q)";
 prove "disj_not2" "(P | ~Q) = (Q --> P)"; (* changes orientation :-( *)
 
-(*Avoids duplication of subgoals after expand_if, when the true and false 
+(*Avoids duplication of subgoals after split_if, when the true and false 
   cases boil down to the same thing.*) 
 prove "cases_simp" "((P --> Q) & (~P --> Q)) = Q";
 
@@ -261,27 +261,29 @@
 qed_goalw "if_not_P" HOL.thy [if_def] "!!P. ~P ==> (if P then x else y) = y"
  (K [Blast_tac 1]);
 
-qed_goal "expand_if" HOL.thy
+qed_goal "split_if" HOL.thy
     "P(if Q then x else y) = ((Q --> P(x)) & (~Q --> P(y)))" (K [
 	res_inst_tac [("Q","Q")] (excluded_middle RS disjE) 1,
          stac if_P 2,
          stac if_not_P 1,
          ALLGOALS (Blast_tac)]);
+(* for backwards compatibility: *)
+val expand_if = split_if;
 
 qed_goal "split_if_asm" HOL.thy
     "P(if Q then x else y) = (~((Q & ~P x) | (~Q & ~P y)))"
-    (K [stac expand_if 1,
+    (K [stac split_if 1,
 	Blast_tac 1]);
 
 (*This form is useful for expanding IFs on the RIGHT of the ==> symbol*)
 qed_goal "if_bool_eq_conj" HOL.thy
     "(if P then Q else R) = ((P-->Q) & (~P-->R))"
-    (K [rtac expand_if 1]);
+    (K [rtac split_if 1]);
 
 (*And this form is useful for expanding IFs on the LEFT*)
 qed_goal "if_bool_eq_disj" HOL.thy
     "(if P then Q else R) = ((P&Q) | (~P&R))"
-    (K [stac expand_if 1,
+    (K [stac split_if 1,
 	Blast_tac 1]);
 
 
@@ -359,10 +361,10 @@
 fun Delsplits splits = (simpset_ref() := simpset() delsplits splits);
 
 qed_goal "if_cancel" HOL.thy "(if c then x else x) = x"
-  (K [split_tac [expand_if] 1, Blast_tac 1]);
+  (K [split_tac [split_if] 1, Blast_tac 1]);
 
 qed_goal "if_eq_cancel" HOL.thy "(if x = y then y else x) = x"
-  (K [split_tac [expand_if] 1, Blast_tac 1]);
+  (K [split_tac [split_if] 1, Blast_tac 1]);
 
 (** 'if' congruence rules: neither included by default! *)
 
@@ -371,7 +373,7 @@
   "[| b=c; c ==> x=u; ~c ==> y=v |] ==>\
 \  (if b then x else y) = (if c then u else v)"
   (fn rew::prems =>
-   [stac rew 1, stac expand_if 1, stac expand_if 1,
+   [stac rew 1, stac split_if 1, stac split_if 1,
     blast_tac (HOL_cs addDs prems) 1]);
 
 (*Prevents simplification of x and y: much faster*)
@@ -418,11 +420,11 @@
      @ ex_simps @ all_simps @ simp_thms)
      addsimprocs [defALL_regroup,defEX_regroup]
      addcongs [imp_cong]
-     addsplits [expand_if];
+     addsplits [split_if];
 
 qed_goal "if_distrib" HOL.thy
   "f(if c then x else y) = (if c then f x else f y)" 
-  (K [simp_tac (HOL_ss setloop (split_tac [expand_if])) 1]);
+  (K [simp_tac (HOL_ss setloop (split_tac [split_if])) 1]);
 
 qed_goalw "o_assoc" HOL.thy [o_def] "f o (g o h) = f o g o h"
   (K [rtac ext 1, rtac refl 1]);