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.
avoid global syntax for MinProof (amending e31271559de8);
authorwenzelm
Wed, 24 Jul 2019 10:49:01 +0200
changeset 70403 468cfd56ee03
parent 70402 29d81b53c40b
child 70404 9dc99e3153b3
avoid global syntax for MinProof (amending e31271559de8);
src/Pure/pure_thy.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/pure_thy.ML	Tue Jul 23 23:10:22 2019 +0200
+++ b/src/Pure/pure_thy.ML	Wed Jul 24 10:49:01 2019 +0200
@@ -224,7 +224,7 @@
     (qualify (Binding.make ("Hyp", \<^here>)), typ "prop \<Rightarrow> Pure.proof", NoSyn),
     (qualify (Binding.make ("Oracle", \<^here>)), typ "prop \<Rightarrow> Pure.proof", NoSyn),
     (qualify (Binding.make ("OfClass", \<^here>)), typ "('a itself \<Rightarrow> prop) \<Rightarrow> Pure.proof", NoSyn),
-    (qualify (Binding.make ("MinProof", \<^here>)), typ "Pure.proof", Mixfix.mixfix "?")]
+    (qualify (Binding.make ("MinProof", \<^here>)), typ "Pure.proof", NoSyn)]
   #> add_deps_const "Pure.eq"
   #> add_deps_const "Pure.imp"
   #> add_deps_const "Pure.all"
isabelle