src/HOL/Enum.thy
changeset 40659 b26afaa55a75
parent 40657 58a6ba7ccfc5
child 40683 a3f37b3d303a
equal deleted inserted replaced
40658:5ccfc3ee7fe6 40659:b26afaa55a75
   451 
   451 
   452 hide_const a\<^isub>1 a\<^isub>2 a\<^isub>3 a\<^isub>4 a\<^isub>5
   452 hide_const a\<^isub>1 a\<^isub>2 a\<^isub>3 a\<^isub>4 a\<^isub>5
   453 
   453 
   454 
   454 
   455 hide_type finite_1 finite_2 finite_3 finite_4 finite_5
   455 hide_type finite_1 finite_2 finite_3 finite_4 finite_5
   456 hide_const (open) n_lists product
   456 hide_const (open) enum n_lists product
   457 
   457 
   458 end
   458 end