src/HOL/Induct/Tree.thy
changeset 39246 9e58f0499f57
parent 35439 888993948a1d
child 46914 c2ca2c3d23a6
     1.1 --- a/src/HOL/Induct/Tree.thy	Wed Sep 08 13:25:22 2010 +0200
     1.2 +++ b/src/HOL/Induct/Tree.thy	Wed Sep 08 19:21:46 2010 +0200
     1.3 @@ -95,15 +95,15 @@
     1.4  text{*Example of a general function*}
     1.5  
     1.6  function
     1.7 -  add2 :: "(brouwer*brouwer) => brouwer"
     1.8 +  add2 :: "brouwer \<Rightarrow> brouwer \<Rightarrow> brouwer"
     1.9  where
    1.10 -  "add2 (i, Zero) = i"
    1.11 -| "add2 (i, (Succ j)) = Succ (add2 (i, j))"
    1.12 -| "add2 (i, (Lim f)) = Lim (\<lambda> n. add2 (i, (f n)))"
    1.13 +  "add2 i Zero = i"
    1.14 +| "add2 i (Succ j) = Succ (add2 i j)"
    1.15 +| "add2 i (Lim f) = Lim (\<lambda>n. add2 i (f n))"
    1.16  by pat_completeness auto
    1.17  termination by (relation "inv_image brouwer_order snd") auto
    1.18  
    1.19 -lemma add2_assoc: "add2 (add2 (i, j), k) = add2 (i, add2 (j, k))"
    1.20 +lemma add2_assoc: "add2 (add2 i j) k = add2 i (add2 j k)"
    1.21    by (induct k) auto
    1.22  
    1.23  end