# HG changeset patch # User blanchet # Date 1400500438 -7200 # Node ID 61855ade6c7e55694b7569ec01584a0585835376 # Parent 8d5e5ec1cac3ab4f697e632f9df2fbacbb0e2027 hide more consts to beautify documentation diff -r 8d5e5ec1cac3 -r 61855ade6c7e src/Doc/Datatypes/Datatypes.thy --- a/src/Doc/Datatypes/Datatypes.thy Mon May 19 13:44:13 2014 +0200 +++ b/src/Doc/Datatypes/Datatypes.thy Mon May 19 13:53:58 2014 +0200 @@ -194,7 +194,7 @@ *} (*<*) - hide_const None Some + hide_const None Some map_option hide_type option (*>*) datatype_new 'a option = None | Some 'a @@ -367,7 +367,7 @@ Cons (infixr "#" 65) hide_type list - hide_const Nil Cons hd tl set map list_all2 + hide_const Nil Cons hd tl set map list_all2 rec_list size_list context early begin (*>*) diff -r 8d5e5ec1cac3 -r 61855ade6c7e src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon May 19 13:44:13 2014 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML Mon May 19 13:53:58 2014 +0200 @@ -991,6 +991,7 @@ fun fact_has_right_theory (_, th) = thy_name = Context.theory_name (theory_of_thm th) + fun chained_or_extra_features_of factor (((_, stature), th), weight) = [prop_of th] |> features_of ctxt (theory_of_thm th) num_facts const_tab stature false