# HG changeset patch
# User nipkow
# Date 860164059 -7200
# Node ID 8a680e310f041ec3024d86a4a599784e4f38d13e
# Parent  905aa895136cca164e635ea918ab3a640480d027
Inv -> inv

diff -r 905aa895136c -r 8a680e310f04 src/HOL/ex/LList.ML
--- a/src/HOL/ex/LList.ML	Fri Apr 04 16:16:35 1997 +0200
+++ b/src/HOL/ex/LList.ML	Fri Apr 04 16:27:39 1997 +0200
@@ -557,7 +557,7 @@
 (** llist_case: case analysis for 'a llist **)
 
 Addsimps ([Abs_llist_inverse, Rep_llist_inverse,
-           Rep_llist, rangeI, inj_Leaf, Inv_f_f] @ llist.intrs);
+           Rep_llist, rangeI, inj_Leaf, inv_f_f] @ llist.intrs);
 
 goalw LList.thy [llist_case_def,LNil_def]  "llist_case c d LNil = c";
 by (Simp_tac 1);
diff -r 905aa895136c -r 8a680e310f04 src/HOL/ex/LList.thy
--- a/src/HOL/ex/LList.thy	Fri Apr 04 16:16:35 1997 +0200
+++ b/src/HOL/ex/LList.thy	Fri Apr 04 16:27:39 1997 +0200
@@ -89,7 +89,7 @@
 
   llist_case_def
    "llist_case c d l == 
-       List_case c (%x y. d (Inv Leaf x) (Abs_llist y)) (Rep_llist l)"
+       List_case c (%x y. d (inv Leaf x) (Abs_llist y)) (Rep_llist l)"
 
   LList_corec_fun_def
     "LList_corec_fun k f == 
diff -r 905aa895136c -r 8a680e310f04 src/HOL/ex/SList.ML
--- a/src/HOL/ex/SList.ML	Fri Apr 04 16:16:35 1997 +0200
+++ b/src/HOL/ex/SList.ML	Fri Apr 04 16:27:39 1997 +0200
@@ -202,7 +202,7 @@
 local
   val list_rec_simps = [List_rec_NIL, List_rec_CONS, 
                         Abs_list_inverse, Rep_list_inverse,
-                        Rep_list, rangeI, inj_Leaf, Inv_f_f,
+                        Rep_list, rangeI, inj_Leaf, inv_f_f,
                         sexp.LeafI, Rep_list_in_sexp]
 in
   val list_rec_Nil = prove_goalw SList.thy [list_rec_def, Nil_def]
diff -r 905aa895136c -r 8a680e310f04 src/HOL/ex/SList.thy
--- a/src/HOL/ex/SList.thy	Fri Apr 04 16:16:35 1997 +0200
+++ b/src/HOL/ex/SList.thy	Fri Apr 04 16:27:39 1997 +0200
@@ -92,7 +92,7 @@
 
   list_rec_def
    "list_rec l c d == 
-   List_rec (Rep_list l) c (%x y r. d (Inv Leaf x) (Abs_list y) r)"
+   List_rec (Rep_list l) c (%x y r. d (inv Leaf x) (Abs_list y) r)"
 
   (* Generalized Map Functionals *)
 
diff -r 905aa895136c -r 8a680e310f04 src/HOL/ex/Simult.ML
--- a/src/HOL/ex/Simult.ML	Fri Apr 04 16:16:35 1997 +0200
+++ b/src/HOL/ex/Simult.ML	Fri Apr 04 16:27:39 1997 +0200
@@ -280,7 +280,7 @@
    TCONS_I, FNIL_I, FCONS_I, Rep_Tree, Rep_Forest,
    Rep_Tree_inverse, Rep_Forest_inverse,
    Abs_Tree_inverse, Abs_Forest_inverse,
-   inj_Leaf, Inv_f_f, sexp.LeafI, range_eqI,
+   inj_Leaf, inv_f_f, sexp.LeafI, range_eqI,
    Rep_Tree_in_sexp, Rep_Forest_in_sexp];
 
 goalw Simult.thy [tree_rec_def, forest_rec_def, Tcons_def]
diff -r 905aa895136c -r 8a680e310f04 src/HOL/ex/Simult.thy
--- a/src/HOL/ex/Simult.thy	Fri Apr 04 16:16:35 1997 +0200
+++ b/src/HOL/ex/Simult.thy	Fri Apr 04 16:27:39 1997 +0200
@@ -72,11 +72,11 @@
 
   tree_rec_def
    "tree_rec t b c d == 
-   TF_rec (Rep_Tree t) (%x y r. b (Inv Leaf x) (Abs_Forest y) r) 
+   TF_rec (Rep_Tree t) (%x y r. b (inv Leaf x) (Abs_Forest y) r) 
           c (%x y rt rf. d (Abs_Tree x) (Abs_Forest y) rt rf)"
 
   forest_rec_def
    "forest_rec tf b c d == 
-   TF_rec (Rep_Forest tf) (%x y r. b (Inv Leaf x) (Abs_Forest y) r) 
+   TF_rec (Rep_Forest tf) (%x y r. b (inv Leaf x) (Abs_Forest y) r) 
           c (%x y rt rf. d (Abs_Tree x) (Abs_Forest y) rt rf)"
 end
diff -r 905aa895136c -r 8a680e310f04 src/HOL/ex/Term.ML
--- a/src/HOL/ex/Term.ML	Fri Apr 04 16:16:35 1997 +0200
+++ b/src/HOL/ex/Term.ML	Fri Apr 04 16:27:39 1997 +0200
@@ -161,7 +161,7 @@
   val term_rec_ss = HOL_ss
       addsimps [Rep_Tlist RS (rangeI RS term.APP_I RS Abs_term_inverse),  
                 Rep_term_in_sexp, Rep_Term_rec, Rep_term_inverse, inj_Leaf,
-                Inv_f_f, Abs_Rep_map, map_ident2, sexp.LeafI]
+                inv_f_f, Abs_Rep_map, map_ident2, sexp.LeafI]
 in
 
 val term_rec = prove_goalw Term.thy
diff -r 905aa895136c -r 8a680e310f04 src/HOL/ex/Term.thy
--- a/src/HOL/ex/Term.thy	Fri Apr 04 16:16:35 1997 +0200
+++ b/src/HOL/ex/Term.thy	Fri Apr 04 16:27:39 1997 +0200
@@ -45,7 +45,7 @@
 
   term_rec_def
    "term_rec t d == 
-   Term_rec (Rep_term t) (%x y r. d (Inv Leaf x) (Abs_Tlist(y)) r)"
+   Term_rec (Rep_term t) (%x y r. d (inv Leaf x) (Abs_Tlist(y)) r)"
 
 rules
     (*faking a type definition for term...*)
diff -r 905aa895136c -r 8a680e310f04 src/HOL/ex/set.ML
--- a/src/HOL/ex/set.ML	Fri Apr 04 16:16:35 1997 +0200
+++ b/src/HOL/ex/set.ML	Fri Apr 04 16:27:39 1997 +0200
@@ -43,11 +43,11 @@
 
 (*** The Schroder-Berstein Theorem ***)
 
-val prems = goalw Lfp.thy [image_def] "inj(f) ==> Inv(f)``(f``X) = X";
+val prems = goalw Lfp.thy [image_def] "inj(f) ==> inv(f)``(f``X) = X";
 by (cut_facts_tac prems 1);
 by (rtac equalityI 1);
-by (fast_tac (!claset addEs [Inv_f_f RS ssubst]) 1);
-by (fast_tac (!claset addEs [Inv_f_f RS ssubst]) 1);
+by (fast_tac (!claset addEs [inv_f_f RS ssubst]) 1);
+by (fast_tac (!claset addEs [inv_f_f RS ssubst]) 1);
 qed "inv_image_comp";
 
 goal Set.thy "!!f. f(a) ~: (f``X) ==> a~:X";
@@ -116,7 +116,7 @@
 by (rtac exI 1);
 by (rtac bij_if_then_else 1);
 by (EVERY [rtac refl 4, rtac (injf RS inj_imp) 1,
-           rtac (injg RS inj_onto_Inv) 1]);
+           rtac (injg RS inj_onto_inv) 1]);
 by (EVERY1 [etac ssubst, stac double_complement, rtac subsetI,
             etac imageE, etac ssubst, rtac rangeI]);
 by (EVERY1 [etac ssubst, stac double_complement,