equal
deleted
inserted
replaced
2 imports Main |
2 imports Main |
3 uses "mutabelle.ML" |
3 uses "mutabelle.ML" |
4 begin |
4 begin |
5 |
5 |
6 ML {* |
6 ML {* |
7 val comms = [@{const_name "op ="}, @{const_name HOL.disj}, @{const_name HOL.conj}]; |
7 val comms = [@{const_name HOL.eq}, @{const_name HOL.disj}, @{const_name HOL.conj}]; |
8 |
8 |
9 val forbidden = |
9 val forbidden = |
10 [(@{const_name Power.power}, "'a"), |
10 [(@{const_name Power.power}, "'a"), |
11 (@{const_name HOL.induct_equal}, "'a"), |
11 (@{const_name HOL.induct_equal}, "'a"), |
12 (@{const_name HOL.induct_implies}, "'a"), |
12 (@{const_name HOL.induct_implies}, "'a"), |