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