Re: [isabelle] How to fix it?
> Ok, it seem's working, thanks very very much. I've added CPure and HOL
> at imports's field.
For normal applications, you should always import "Main" (which CPure
and HOL). Then the primrec command is available.
> consts neg_eq :: "sbf => sbf"
> "neg_eq(P) = P"
> "neg_eq((Neg(P))) = Neg(P)"
> "neg_eq((Neg(Neg(P)))) = neg_eq(P)"
Primrec can only do primitive recursion over inductive datatypes (i.e.
you define them via the "datatype" command). So even if you import Main,
this will fail.
> I'm trying to prove that every possible proposicional formula can be
> wrriten using
> one or any negations in front of.
For that, you need to define your formulae as an inductive datatype,
just as a type of lists or trees (see Tutorial).
This archive was generated by a fusion of
Pipermail (Mailman edition) and