# HG changeset patch # User nipkow # Date 860158120 -7200 # Node ID d1d5a0acbf7249ff33a488ce5b26cc3cb9b4802d # Parent bacef535265c0de3f20d77f8393d94123ef61515 Inv -> inv diff -r bacef535265c -r d1d5a0acbf72 src/HOL/Subst/UTerm.ML --- 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); diff -r bacef535265c -r d1d5a0acbf72 src/HOL/Subst/UTerm.thy --- 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