src/HOL/Mutabelle/Mutabelle.thy
changeset 38864 4abe644fcea5
parent 38795 848be46708dc
child 39557 fe5722fce758
     1.1 --- a/src/HOL/Mutabelle/Mutabelle.thy	Sat Aug 28 20:24:40 2010 +0800
     1.2 +++ b/src/HOL/Mutabelle/Mutabelle.thy	Sat Aug 28 16:14:32 2010 +0200
     1.3 @@ -4,7 +4,7 @@
     1.4  begin
     1.5  
     1.6  ML {*
     1.7 -val comms = [@{const_name "op ="}, @{const_name HOL.disj}, @{const_name HOL.conj}];
     1.8 +val comms = [@{const_name HOL.eq}, @{const_name HOL.disj}, @{const_name HOL.conj}];
     1.9  
    1.10  val forbidden =
    1.11   [(@{const_name Power.power}, "'a"),