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.
Goal: tuned pris;
authorwenzelm
Mon, 29 Nov 1999 15:52:49 +0100
changeset 8039 a901bafe4578
parent 8038 a13c3b80d3d4
child 8040 23e2a2457c77
Goal: tuned pris;
src/Pure/pure_thy.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/pure_thy.ML	Mon Nov 29 14:12:53 1999 +0100
+++ b/src/Pure/pure_thy.ML	Mon Nov 29 15:52:49 1999 +0100
@@ -435,11 +435,11 @@
     ("=?=", "['a::{}, 'a] => prop", InfixrName ("=?=", 2)),
     ("==>", "[prop, prop] => prop", Mixfix ("(_/ ==> _)", [2, 1], 1)),
     ("all", "('a => prop) => prop", Binder ("!!", 0, 0)),
-    ("Goal", "prop => prop", Mixfix ("GOAL _", [999], 1000)),
+    ("Goal", "prop => prop", Mixfix ("GOAL _", [1000], 999)),
     ("TYPE", "'a itself", NoSyn),
     (dummy_patternN, "'a", Delimfix "'_")]
   |> Theory.add_modesyntax ("", false)
-    [("Goal", "prop => prop", Mixfix ("_", [0], 1000))]
+    [("Goal", "prop => prop", Mixfix ("_", [0], 0))]
   |> local_path
   |> (add_defs o map Thm.no_attributes)
    [("flexpair_def", "(t =?= u) == (t == u::'a::{})"),
isabelle