Commit 63857b89 authored by Raphael Cauderlier's avatar Raphael Cauderlier
Browse files

Merge branch 'master' of gitlab.math.univ-paris-diderot.fr:cauderlier/math_transfer

Conflicts:
	interop/arith/Makefile
	interop/arith/natural_coq.fcl
	interop/arith/natural_hol.fcl
parents fedcd127 2bbd2908
......@@ -21,10 +21,10 @@ let hsucc (n : hnat) = internal hnat
| dedukti -> {* natural__div__full.Number_2ENatural_2Esuc n *};;
theorem hol_induction :
all p : hnat -> prop,
(p(hzero) /\ (all n : hnat, p(n) -> p(hsucc(n)))) ->
(all n : hnat, p(n))
proof = dedukti proof {* natural__div__full.thm_3723. *};;
all p : hnat -> bool,
(p(hzero) /\ (all n : hnat, p(n) -> p(hsucc(n)))) ->
(all n : hnat, p(n))
proof = dedukti proof {* natural__div__full.thm_3723. *};;
species HolNatDecl =
inherit NatDecl;
......
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