Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
clarified options, following e.g. "show_consts";
authorwenzelm
Mon, 05 Sep 2022 22:47:09 +0200
changeset 76068 319d08115b13
parent 76067 e39c1da9d904
child 76069 79094d7b6f22
clarified options, following e.g. "show_consts";
etc/options file | annotate | diff | comparison | revisions
src/Pure/Isar/proof_display.ML file | annotate | diff | comparison | revisions 
--- a/etc/options	Mon Sep 05 21:59:05 2022 +0200
+++ b/etc/options	Mon Sep 05 22:47:09 2022 +0200
@@ -59,6 +59,8 @@
 
 option show_consts : bool = false
   -- "show constants with types when printing proof state"
+option show_goal_inst : bool = false
+  -- "show goal instantiation (for schematic goals)"
 option show_main_goal : bool = false
   -- "show main goal when printing proof state"
 option goals_limit : int = 10
--- a/src/Pure/Isar/proof_display.ML	Mon Sep 05 21:59:05 2022 +0200
+++ b/src/Pure/Isar/proof_display.ML	Mon Sep 05 22:47:09 2022 +0200
@@ -248,7 +248,7 @@
 
 (* goal instantiation *)
 
-val show_goal_inst = Attrib.setup_config_bool \<^binding>\<open>show_goal_inst\<close> (K false);
+val show_goal_inst = Attrib.setup_option_bool ("show_goal_inst", \<^here>);
 
 fun pretty_goal_inst ctxt propss goal =
   let
isabelle