changeset 38795 | 848be46708dc |
parent 36610 | bafd82950e24 |
child 38864 | 4abe644fcea5 |
--- a/src/HOL/Mutabelle/Mutabelle.thy Fri Aug 27 10:55:20 2010 +0200 +++ b/src/HOL/Mutabelle/Mutabelle.thy Fri Aug 27 10:56:46 2010 +0200 @@ -4,7 +4,7 @@ begin ML {* -val comms = [@{const_name "op ="}, @{const_name "op |"}, @{const_name "op &"}]; +val comms = [@{const_name "op ="}, @{const_name HOL.disj}, @{const_name HOL.conj}]; val forbidden = [(@{const_name Power.power}, "'a"),