hide new constants
authorhaftmann
Tue Sep 15 19:16:35 2009 +0200 (2009-09-15)
changeset 32582a382876d3290
parent 32581 44ac2e398411
child 32583 986cba8c5053
hide new constants
src/HOL/Predicate.thy
     1.1 --- a/src/HOL/Predicate.thy	Tue Sep 15 15:41:30 2009 +0200
     1.2 +++ b/src/HOL/Predicate.thy	Tue Sep 15 19:16:35 2009 +0200
     1.3 @@ -874,7 +874,7 @@
     1.4    bind (infixl "\<guillemotright>=" 70)
     1.5  
     1.6  hide (open) type pred seq
     1.7 -hide (open) const Pred eval single bind if_pred not_pred
     1.8 -  Empty Insert Join Seq member pred_of_seq "apply" adjunct eq map
     1.9 +hide (open) const Pred eval single bind is_empty singleton if_pred not_pred
    1.10 +  Empty Insert Join Seq member pred_of_seq "apply" adjunct null the_only eq map
    1.11  
    1.12  end