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.
tuned Goal syntax;
authorwenzelm
Thu, 19 Aug 1999 12:47:45 +0200
changeset 7278 da64f7413efd
parent 7277 bb9502f9154a
child 7279 8cc108434750
tuned Goal syntax;
src/Pure/pure_thy.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/pure_thy.ML	Thu Aug 19 12:43:02 1999 +0200
+++ b/src/Pure/pure_thy.ML	Thu Aug 19 12:47:45 1999 +0200
@@ -432,7 +432,7 @@
     ("TYPE", "'a itself", NoSyn),
     (dummy_patternN, "'a", Delimfix "'_")]
   |> Theory.add_modesyntax ("", false)
-    [("Goal", "prop => prop", Mixfix ("_", [0], 0))]
+    [("Goal", "prop => prop", Mixfix ("_", [0], 1000))]
   |> local_path
   |> (add_defs o map Thm.no_attributes)
    [("flexpair_def", "(t =?= u) == (t == u::'a::{})"),
isabelle