Skip to content

Commit

Permalink
fixing ambitous find and replace
Browse files Browse the repository at this point in the history
  • Loading branch information
zstone1 committed Oct 23, 2024
1 parent 7a8dbae commit c6288d4
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion theories/lebesgue_integral.v
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@ From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap.
From mathcomp Require Import archimedean.
From mathcomp Require Import boolp classical_sets functions.
From mathcomp Require Import cardinality fsbigop.
Require Import signed reals ereal topologyype sequences real_interval.
Require Import signed reals ereal topology normedtype sequences real_interval.
Require Import esum measure lebesgue_measure numfun realfun function_spaces.

(**md**************************************************************************)
Expand Down

0 comments on commit c6288d4

Please sign in to comment.