mn200/HOL — Issue #44: STRIP_QUANT_CONV unexpected behaviour
Author: xrchz
Created: 2011-11-04 12:34:16+00:00
State: open

```> val c = let open Canon in NNF_CONV NO_CONV true THENC PROP_CNF_CONV end;

> t';
val it =
``∀y. ∃x. ∀x'. x ∧ y ∨ (y ⇒ x')``:
term

> (STRIP_QUANT_CONV c) t';
val it =
|- (∀y. ∃x. ∀x'. x ∧ y ∨ (y ⇒ x')) ⇔ ∀y. ∃x. ∀x'. x ∧ y ∨ x' ∨ ¬y:
thm

> t'';
val it =
``x ∧ y ∨ (y ⇒ x')``:
term

> c t'';
val it =
|- x ∧ y ∨ (y ⇒ x') ⇔ (x ∨ x' ∨ ¬y) ∧ (y ∨ x' ∨ ¬y):
thm```

Shouldn't the rhs above be the same as the body in the result of STRIP_QUANT_CONV?