- Nov 01, 2019
-
-
Ralf Jung authored
-
- Sep 11, 2019
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
- Aug 16, 2019
-
-
Robbert Krebbers authored
-
- May 01, 2019
-
-
Robbert Krebbers authored
-
Dan Frumin authored
-
Dan Frumin authored
-
- Apr 23, 2019
-
-
Robbert Krebbers authored
-
- Apr 17, 2019
-
-
Robbert Krebbers authored
-
- Feb 16, 2019
-
-
Ralf Jung authored
-
- Jan 23, 2019
-
-
Mackie Loeffel authored
-
- Jan 14, 2019
-
-
Tej Chajed authored
-
- Jan 11, 2019
-
-
Robbert Krebbers authored
It now supports the specialization pattern `(H spat1 .. spatn)`, which first recursively specializes the hypothesis `H` using the specialization patterns `spat1 .. spatn`.
-
Robbert Krebbers authored
This commit closes issue #192.
-
- Dec 25, 2018
-
-
Robbert Krebbers authored
-
- May 30, 2018
-
-
Robbert Krebbers authored
-
- May 18, 2018
-
-
Robbert Krebbers authored
This fixes issue #187.
-
- Mar 04, 2018
-
-
Robbert Krebbers authored
sed -i 's/absolute/objective/g; s/relative/subjective/g; s/Absolute/Objective/g; s/Relative/Subjective/g' $(find ./ -name \*.v)
-
- Mar 03, 2018
-
-
Robbert Krebbers authored
-
- Feb 28, 2018
-
-
Robbert Krebbers authored
-
- Feb 23, 2018
-
-
Joseph Tassarotti authored
-
Joseph Tassarotti authored
-
- Feb 19, 2018
-
-
Robbert Krebbers authored
-
- Jan 23, 2018
-
-
Robbert Krebbers authored
-
- Oct 27, 2017
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
This closes issue #64.
-
Ralf Jung authored
-
- Oct 26, 2017
-
-
Robbert Krebbers authored
-
- Aug 04, 2017
-
-
Robbert Krebbers authored
-
- Apr 27, 2017
-
-
Robbert Krebbers authored
Now they can also be used to clear/frame the whole pure/persistent/spatial context.
-
- Mar 28, 2017
-
-
Robbert Krebbers authored
-
- Mar 16, 2017
-
-
Robbert Krebbers authored
This fixes issue #81.
-
Dan Frumin authored
-
Dan Frumin authored
-
- Mar 14, 2017
-
-
Robbert Krebbers authored
-
Robbert Krebbers authored
-
Robbert Krebbers authored
- Support for a `//` modifier to close the goal using `done`. - Support for framing in the `[#]` specialization pattern for persistent premises, i.e. `[# $H1 $H2]` - Add new "auto framing patterns" `[$]`, `[# $]` and `>[$]` that will try to solve the premise by framing. Hypothesis that are not framed are carried over to the next goal.
-
- Mar 07, 2017
-
-
Robbert Krebbers authored
-
- Feb 17, 2017
-
-
Robbert Krebbers authored
-
- Jan 24, 2017
-
-
Robbert Krebbers authored
-