190 |
190 |
191 val comms = [@{const_name "op ="}, @{const_name "op |"}, @{const_name "op &"}] |
191 val comms = [@{const_name "op ="}, @{const_name "op |"}, @{const_name "op &"}] |
192 |
192 |
193 val forbidden = |
193 val forbidden = |
194 [(* (@{const_name "power"}, "'a"), *) |
194 [(* (@{const_name "power"}, "'a"), *) |
195 (@{const_name HOL.induct_equal}, "'a"), |
195 (*(@{const_name induct_equal}, "'a"), |
196 (@{const_name HOL.induct_implies}, "'a"), |
196 (@{const_name induct_implies}, "'a"), |
197 (@{const_name HOL.induct_conj}, "'a"), |
197 (@{const_name induct_conj}, "'a"),*) |
198 (@{const_name "undefined"}, "'a"), |
198 (@{const_name "undefined"}, "'a"), |
199 (@{const_name "default"}, "'a"), |
199 (@{const_name "default"}, "'a"), |
200 (@{const_name "dummy_pattern"}, "'a::{}") (*, |
200 (@{const_name "dummy_pattern"}, "'a::{}") (*, |
201 (@{const_name "uminus"}, "'a"), |
201 (@{const_name "uminus"}, "'a"), |
202 (@{const_name "Nat.size"}, "'a"), |
202 (@{const_name "Nat.size"}, "'a"), |