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.
give up show_main_goal (despite 922e3f9251ac): show_goal_inst is sufficient, even for final results;
authorwenzelm
Thu, 08 Sep 2022 22:59:21 +0200
changeset 76094 4dec713d3bc9
parent 76093 ce66ff654e59
child 76095 7cac5565e79b
give up show_main_goal (despite 922e3f9251ac): show_goal_inst is sufficient, even for final results;
src/HOL/Prolog/HOHH.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Prolog/HOHH.thy	Thu Sep 08 22:35:50 2022 +0200
+++ b/src/HOL/Prolog/HOHH.thy	Thu Sep 08 22:59:21 2022 +0200
@@ -10,8 +10,6 @@
 
 ML_file \<open>prolog.ML\<close>
 
-declare [[show_main_goal]]
-
 method_setup ptac =
   \<open>Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD' (Prolog.ptac ctxt thms))\<close>
   "basic Lambda Prolog interpreter"
isabelle