Skip to content
GitLab
Explore
Sign in
Iris
Iris
Merge requests
Open
20
Merged
909
Closed
118
All
1,047
Actions
Subscribe to RSS feed
Recent searches
{{formattedKey}}
{{ title }}
{{ help }}
{{name}}
@{{username}}
None
Any
{{name}}
@{{username}}
None
Any
{{name}}
@{{username}}
None
Any
{{name}}
@{{username}}
None
Any
Upcoming
Started
{{title}}
None
Any
{{title}}
None
Any
{{title}}
None
Any
{{name}}
Yes
No
Yes
No
{{title}}
{{title}}
{{title}}
Updated date
Store a counter in `Envs` to assign fresh names with `iFresh`.
!128
· created
Mar 12, 2018
by
Joseph Tassarotti
gen_proofmode
Merged
10
updated
Mar 15, 2018
Renaming and notations for modalities gen_proofmode
!126
· created
Mar 04, 2018
by
Robbert Krebbers
gen_proofmode
Merged
5
updated
Mar 04, 2018
Make iFrame able to accumulate assertions in an evar.
!124
· created
Mar 01, 2018
by
Jacques-Henri Jourdan
gen_proofmode
Merged
10
updated
Mar 03, 2018
Bundle classes for updates, plainly and embeddings
!125
· created
Mar 02, 2018
by
Robbert Krebbers
gen_proofmode
Merged
50
updated
Mar 03, 2018
Get rid of `FromLaterN` class.
!123
· created
Mar 01, 2018
by
Robbert Krebbers
gen_proofmode
Merged
15
updated
Mar 03, 2018
Factor plainly out of main BI interface
!98
· created
Dec 06, 2017
by
Ralf Jung
Generalized Proofmode Merger
gen_proofmode
T-proofmode
Closed
171
updated
Mar 03, 2018
Repair the plainly modality
!122
· created
Feb 23, 2018
by
Robbert Krebbers
gen_proofmode
Merged
1
32
updated
Feb 26, 2018
Fix regression in iGPS caused by eebe055b958d6db12ef5ccd2718bc3c952438483.
!120
· created
Feb 22, 2018
by
Robbert Krebbers
Merged
3
updated
Feb 23, 2018
Syntax `iAssert (Q with spat) as ...`
!117
· created
Feb 19, 2018
by
Robbert Krebbers
gen_proofmode
Closed
8
updated
Feb 21, 2018
weaken BI axiom persistently_and_sep_elim and re-derive the stronger form
!119
· created
Feb 21, 2018
by
Ralf Jung
gen_proofmode
Merged
0
updated
Feb 21, 2018
Bring back side-conditionals for `iMod`
!113
· created
Feb 12, 2018
by
Robbert Krebbers
gen_proofmode
Merged
7
updated
Feb 15, 2018
Set mode for update modalities
!115
· created
Feb 13, 2018
by
Ralf Jung
gen_proofmode
T-proofmode
Merged
32
updated
Feb 14, 2018
Special proof mode class for adding a modality to a goal
!107
· created
Jan 16, 2018
by
Robbert Krebbers
Merged
2
updated
Feb 12, 2018
Use `NoBackTrack` type class for framing with ▷
1 of 1 checklist item completed
!112
· created
Feb 08, 2018
by
Robbert Krebbers
Merged
15
updated
Feb 08, 2018
Various improvements to iFrame
!110
· created
Feb 02, 2018
by
Robbert Krebbers
Merged
19
updated
Feb 08, 2018
Generic `iAlways` tactic.
3 of 3 checklist items completed
!111
· created
Feb 06, 2018
by
Robbert Krebbers
gen_proofmode
Merged
23
updated
Feb 08, 2018
Add stuckness bits to WP.
!80
· created
Nov 09, 2017
by
David Swasey
Iris 3.1
Merged
79
updated
Feb 02, 2018
Make invariants closed under weakening.
!85
· created
Nov 16, 2017
by
Robbert Krebbers
Merged
9
updated
Jan 24, 2018
Consistently name `wp_value_inv`
!108
· created
Jan 19, 2018
by
Robbert Krebbers
Merged
5
updated
Jan 24, 2018
`iEval ... in ...` for performing a tactic in an invidual proofmode hypothesis
!105
· created
Dec 31, 2017
by
Robbert Krebbers
Merged
14
updated
Jan 24, 2018
Prev
1
…
44
45
46
47
48
49
50
51
52
53
Next