Skip to content

Commit

Permalink
chore(analysis/topology): remove complete_groups; this should be now …
Browse files Browse the repository at this point in the history
…in completion
  • Loading branch information
johoelzl committed Sep 25, 2018
1 parent 0efcf99 commit 85b19e2
Showing 1 changed file with 0 additions and 250 deletions.
250 changes: 0 additions & 250 deletions analysis/topology/complete_groups.lean

This file was deleted.

0 comments on commit 85b19e2

Please sign in to comment.