src/Pure/proof_general.ML
changeset 13884 5affbaee6b18
parent 13801 6c5c5bdfae84
child 14557 31ae4a47267c
equal deleted inserted replaced
13883:0451e0fb3f22 13884:5affbaee6b18
   283       bool_option show_sorts)),
   283       bool_option show_sorts)),
   284    ("show-consts", ("Whether to show types of consts in Isabelle goals.",
   284    ("show-consts", ("Whether to show types of consts in Isabelle goals.",
   285       bool_option show_consts)),
   285       bool_option show_consts)),
   286    ("long-names", ("Whether to show fully qualified names in Isabelle.",
   286    ("long-names", ("Whether to show fully qualified names in Isabelle.",
   287       bool_option long_names)),
   287       bool_option long_names)),
       
   288    ("show-brackets", ("Whether to show full bracketing in Isabelle.",
       
   289       bool_option show_brackets)),
   288    ("eta-contract", ("Whether to print terms eta-contracted in Isabelle.",
   290    ("eta-contract", ("Whether to print terms eta-contracted in Isabelle.",
   289       bool_option Syntax.eta_contract)),
   291       bool_option Syntax.eta_contract)),
   290    ("trace-simplifier", ("Whether to trace the Simplifier in Isabelle.",
   292    ("trace-simplifier", ("Whether to trace the Simplifier in Isabelle.",
   291       bool_option trace_simp)),
   293       bool_option trace_simp)),
   292    ("trace-rules", ("Whether to trace the standard rules in Isabelle.",
   294    ("trace-rules", ("Whether to trace the standard rules in Isabelle.",