author | haftmann |
Tue, 15 Sep 2009 19:16:35 +0200 | |
changeset 32582 | a382876d3290 |
parent 32581 | 44ac2e398411 |
child 32583 | 986cba8c5053 |
--- a/src/HOL/Predicate.thy Tue Sep 15 15:41:30 2009 +0200 +++ b/src/HOL/Predicate.thy Tue Sep 15 19:16:35 2009 +0200 @@ -874,7 +874,7 @@ bind (infixl "\<guillemotright>=" 70) hide (open) type pred seq -hide (open) const Pred eval single bind if_pred not_pred - Empty Insert Join Seq member pred_of_seq "apply" adjunct eq map +hide (open) const Pred eval single bind is_empty singleton if_pred not_pred + Empty Insert Join Seq member pred_of_seq "apply" adjunct null the_only eq map end