src/HOL/Predicate.thy
changeset 36176 3fe7e97ccca8
parent 36008 23dfa8678c7c
child 36513 70096cbdd4e0
     1.1 --- a/src/HOL/Predicate.thy	Fri Apr 16 20:56:40 2010 +0200
     1.2 +++ b/src/HOL/Predicate.thy	Fri Apr 16 21:28:09 2010 +0200
     1.3 @@ -934,8 +934,8 @@
     1.4    bot ("\<bottom>") and
     1.5    bind (infixl "\<guillemotright>=" 70)
     1.6  
     1.7 -hide (open) type pred seq
     1.8 -hide (open) const Pred eval single bind is_empty singleton if_pred not_pred holds
     1.9 +hide_type (open) pred seq
    1.10 +hide_const (open) Pred eval single bind is_empty singleton if_pred not_pred holds
    1.11    Empty Insert Join Seq member pred_of_seq "apply" adjunct null the_only eq map not_unique the
    1.12  
    1.13  end