hide more consts to beautify documentation
authorblanchet
Mon May 19 13:53:58 2014 +0200 (2014-05-19)
changeset 5699561855ade6c7e
parent 56994 8d5e5ec1cac3
child 56996 891e992e510f
child 56997 ab28906b54ae
hide more consts to beautify documentation
src/Doc/Datatypes/Datatypes.thy
src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
     1.1 --- a/src/Doc/Datatypes/Datatypes.thy	Mon May 19 13:44:13 2014 +0200
     1.2 +++ b/src/Doc/Datatypes/Datatypes.thy	Mon May 19 13:53:58 2014 +0200
     1.3 @@ -194,7 +194,7 @@
     1.4  *}
     1.5  
     1.6  (*<*)
     1.7 -    hide_const None Some
     1.8 +    hide_const None Some map_option
     1.9      hide_type option
    1.10  (*>*)
    1.11      datatype_new 'a option = None | Some 'a
    1.12 @@ -367,7 +367,7 @@
    1.13        Cons (infixr "#" 65)
    1.14  
    1.15      hide_type list
    1.16 -    hide_const Nil Cons hd tl set map list_all2
    1.17 +    hide_const Nil Cons hd tl set map list_all2 rec_list size_list
    1.18  
    1.19      context early begin
    1.20  (*>*)
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon May 19 13:44:13 2014 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Mon May 19 13:53:58 2014 +0200
     2.3 @@ -991,6 +991,7 @@
     2.4  
     2.5      fun fact_has_right_theory (_, th) =
     2.6        thy_name = Context.theory_name (theory_of_thm th)
     2.7 +
     2.8      fun chained_or_extra_features_of factor (((_, stature), th), weight) =
     2.9        [prop_of th]
    2.10        |> features_of ctxt (theory_of_thm th) num_facts const_tab stature false