src/HOL/Isar_Examples/Summation.thy
changeset 63583 a39baba12732
parent 61932 2e48182cc82c
equal deleted inserted replaced
63582:161c5d8ae266 63583:a39baba12732
     3 *)
     3 *)
     4 
     4 
     5 section \<open>Summing natural numbers\<close>
     5 section \<open>Summing natural numbers\<close>
     6 
     6 
     7 theory Summation
     7 theory Summation
     8 imports Main
     8   imports Main
     9 begin
     9 begin
    10 
    10 
    11 text \<open>
    11 text \<open>
    12   Subsequently, we prove some summation laws of natural numbers (including
    12   Subsequently, we prove some summation laws of natural numbers (including
    13   odds, squares, and cubes). These examples demonstrate how plain natural
    13   odds, squares, and cubes). These examples demonstrate how plain natural