src/HOL/HOL.thy
changeset 56375 32e0da92c786
parent 55757 9fc71814b8c1
child 56941 952833323c99
     1.1 --- a/src/HOL/HOL.thy	Thu Apr 03 10:51:20 2014 +0200
     1.2 +++ b/src/HOL/HOL.thy	Thu Apr 03 10:51:22 2014 +0200
     1.3 @@ -2017,4 +2017,3 @@
     1.4  hide_const (open) eq equal
     1.5  
     1.6  end
     1.7 -