Skip to content
GitLab
Explore
Sign in
Lennard Gäher
Iris
Repository
iris
theories
proofmode
environments.v
Find file
Blame
History
Permalink
Make iPureIntro able to introduce [bi_affinely (bi_pure P)] when the context is empty.
· 36654e76
Jacques-Henri Jourdan
authored
Feb 15, 2018
36654e76