Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Inv -> inv
authornipkow
Fri, 04 Apr 1997 14:48:40 +0200
changeset 2903 d1d5a0acbf72
parent 2902 bacef535265c
child 2904 fc10751254aa
Inv -> inv
src/HOL/Subst/UTerm.ML file | annotate | diff | comparison | revisions
src/HOL/Subst/UTerm.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Subst/UTerm.ML	Fri Apr 04 14:47:26 1997 +0200
+++ b/src/HOL/Subst/UTerm.ML	Fri Apr 04 14:48:40 1997 +0200
@@ -247,7 +247,7 @@
 
 Addsimps [UTerm_rec_VAR, UTerm_rec_CONST, UTerm_rec_COMB, 
           Abs_uterm_inverse, Rep_uterm_inverse, 
-          Rep_uterm, rangeI, inj_Leaf, Inv_f_f, Rep_uterm_in_sexp];
+          Rep_uterm, rangeI, inj_Leaf, inv_f_f, Rep_uterm_in_sexp];
 
 goalw UTerm.thy [uterm_rec_def, Var_def] "uterm_rec (Var x) b c d = b(x)";
 by (Simp_tac 1);
--- a/src/HOL/Subst/UTerm.thy	Fri Apr 04 14:47:26 1997 +0200
+++ b/src/HOL/Subst/UTerm.thy	Fri Apr 04 14:48:40 1997 +0200
@@ -59,7 +59,7 @@
 
   uterm_rec_def
    "uterm_rec t b c d == 
-   UTerm_rec (Rep_uterm t) (%x.b(Inv Leaf x)) (%x.c(Inv Leaf x)) 
+   UTerm_rec (Rep_uterm t) (%x.b(inv Leaf x)) (%x.c(inv Leaf x)) 
                            (%x y q r.d (Abs_uterm x) (Abs_uterm y) q r)"
 
 end
isabelle