changeset 29469 | c03d2db1cda8 |
parent 29353 | 3d2e35c23c66 |
child 29811 | 026b0f9f579f |
29465:b2cfb5d0a59e | 29469:c03d2db1cda8 |
---|---|
4 *) |
4 *) |
5 |
5 |
6 header{*Theory of Integration*} |
6 header{*Theory of Integration*} |
7 |
7 |
8 theory Integration |
8 theory Integration |
9 imports Deriv |
9 imports Deriv ATP_Linkup |
10 begin |
10 begin |
11 |
11 |
12 text{*We follow John Harrison in formalizing the Gauge integral.*} |
12 text{*We follow John Harrison in formalizing the Gauge integral.*} |
13 |
13 |
14 definition |
14 definition |