src/HOL/Partial_Function.thy
changeset 40252 029400b6c893
parent 40107 374f3ef9f940
child 40288 520199d8b66e
     1.1 --- a/src/HOL/Partial_Function.thy	Fri Oct 29 10:40:36 2010 +0200
     1.2 +++ b/src/HOL/Partial_Function.thy	Fri Oct 29 11:04:41 2010 +0200
     1.3 @@ -242,6 +242,7 @@
     1.4    show "option_ord (Option.bind (B f) (\<lambda>y. C y f)) (Option.bind (B g) (\<lambda>y'. C y' g))" .
     1.5  qed
     1.6  
     1.7 +hide_const (open) chain
     1.8  
     1.9  end
    1.10