changeset 38864 | 4abe644fcea5 |
parent 38857 | 97775f3e8722 |
child 39133 | 70d3915c92f0 |
--- a/src/HOL/Mutabelle/mutabelle_extra.ML Sat Aug 28 20:24:40 2010 +0800 +++ b/src/HOL/Mutabelle/mutabelle_extra.ML Sat Aug 28 16:14:32 2010 +0200 @@ -187,7 +187,7 @@ val nitpick_mtd = ("nitpick", invoke_nitpick) *) -val comms = [@{const_name "op ="}, @{const_name HOL.disj}, @{const_name HOL.conj}] +val comms = [@{const_name HOL.eq}, @{const_name HOL.disj}, @{const_name HOL.conj}] val forbidden = [(* (@{const_name "power"}, "'a"), *)