Commit f19927c8 authored by Ulrich's avatar Ulrich


parent 2dfa8d25
......@@ -144,7 +144,7 @@
\begin{frame}{Glivienko's translation}
\begin{frame}{Glivenko's translation}
$A^{glv} := \dneg A$
\it Formula $A$ is a classical tautology if and only if $A^{glv}$ is an intuitionistic tautology.
......@@ -363,7 +363,7 @@ $A^{glv} := \dneg A$
\item help for generating goals and premises during inductions
\item proofs by auto with hint databases
Lemma weakening: forall A B G Z, KIbox Z G B -> KIbox Z (A :: G) B.
......@@ -384,7 +384,7 @@ Lemma eq_kol_kur : forall Z f, KIbox Z [] ((kol f) <<->> (kur f)).
\item a framework for permutations was a big help
\item we should have thought of good tactics earlier\dots}
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment