Backport specification from my PhD thesis
- Feb 10, 2023
-
-
Hans-Jörg Schurr authored
-
Hans-Jörg Schurr authored8cf7e907
-
Hans-Jörg Schurr authored249d8378
-
Hans-Jörg Schurr authored5d255551
-
Hans-Jörg Schurr authored
- adress normalizing of terms with context push (and other typos) - Remark on missing Gamma
bab61d95 -
Hans-Jörg Schurr authored2c28f6f3
-
Hans-Jörg Schurr authored18324875
-
Hans-Jörg Schurr authored99d28a75
-
Haniel Barbosa authored7982cf97
-
Hans-Jörg Schurr authored9dab69e5
-
Hans-Jörg Schurr authored
- replace semantic by semantics - apply some review suggestions
9753d4b7 -
Haniel Barbosa authoredef4f3958
-
Hans-Jörg authoredthis looks less ragged
8efa1d66 -
Hans-Jörg authored
The simplification `(P -> Q) -> Q => P or Q` is already covered by `bool_simplify`.
5f5939fe -
Hans-Jörg authored785e0a3d
-
Hans-Jörg authored03a6e82d
-
Hans-Jörg authored8b912c59
-
Hans-Jörg authoreda8abc836
-
Hans-Jörg authored35219c57
-
Hans-Jörg Schurr authored0b413778
-
Hans-Jörg authored202ceefa
-
Hans-Jörg authoredf4be9e87
-
Hans-Jörg authored68292acb
-
Hans-Jörg authored
- include Changelog - Adapt index tables - Add rule description environments - finish adaption of the proof rule description
f611aa68 -
Hans-Jörg authored
- Add backport goal to Makefile to aid work - copy the main chapter as "spec.tex" - copy the rules appendix as "alethe_rules.tex" - finish adaption of source code in spec.tex
c7b4870d -
Hans-Jörg authored392a7645
-
