src/HOL/ex/Simult.thy
changeset 2911 8a680e310f04
parent 1476 608483c2122a
     1.1 --- a/src/HOL/ex/Simult.thy	Fri Apr 04 16:16:35 1997 +0200
     1.2 +++ b/src/HOL/ex/Simult.thy	Fri Apr 04 16:27:39 1997 +0200
     1.3 @@ -72,11 +72,11 @@
     1.4  
     1.5    tree_rec_def
     1.6     "tree_rec t b c d == 
     1.7 -   TF_rec (Rep_Tree t) (%x y r. b (Inv Leaf x) (Abs_Forest y) r) 
     1.8 +   TF_rec (Rep_Tree t) (%x y r. b (inv Leaf x) (Abs_Forest y) r) 
     1.9            c (%x y rt rf. d (Abs_Tree x) (Abs_Forest y) rt rf)"
    1.10  
    1.11    forest_rec_def
    1.12     "forest_rec tf b c d == 
    1.13 -   TF_rec (Rep_Forest tf) (%x y r. b (Inv Leaf x) (Abs_Forest y) r) 
    1.14 +   TF_rec (Rep_Forest tf) (%x y r. b (inv Leaf x) (Abs_Forest y) r) 
    1.15            c (%x y rt rf. d (Abs_Tree x) (Abs_Forest y) rt rf)"
    1.16  end