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.
CONST syntax with positions;
authorwenzelm
Fri, 08 Apr 2011 21:03:20 +0200
changeset 42296 dcc08f2a8671
parent 42295 8fdbb3b10beb
child 42297 140f283266b7
CONST syntax with positions;
src/Pure/Syntax/syntax_phases.ML file | annotate | diff | comparison | revisions
src/Pure/pure_thy.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Syntax/syntax_phases.ML	Fri Apr 08 20:39:09 2011 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Fri Apr 08 21:03:20 2011 +0200
@@ -667,6 +667,8 @@
         val Const (c', _) = ProofContext.read_const_proper ctxt false c;
         val d = if intern then Lexicon.mark_const c' else c;
       in Ast.Constant d end
+  | const_ast_tr intern ctxt [Ast.Appl [Ast.Constant "_constrain", x, T]] =
+      Ast.Appl [Ast.Constant "_constrain", const_ast_tr intern ctxt [x], T]
   | const_ast_tr _ _ asts = raise Ast.AST ("const_ast_tr", asts);
 
 
--- a/src/Pure/pure_thy.ML	Fri Apr 08 20:39:09 2011 +0200
+++ b/src/Pure/pure_thy.ML	Fri Apr 08 21:03:20 2011 +0200
@@ -137,14 +137,14 @@
     ("_constrain_position", typ "id => id_position",   Delimfix "_"),
     ("_constrain_position", typ "longid => longid_position", Delimfix "_"),
     ("_type_constraint_", typ "'a",                    NoSyn),
-    ("_context_const", typ "id => logic",              Delimfix "CONST _"),
-    ("_context_const", typ "id => aprop",              Delimfix "CONST _"),
-    ("_context_const", typ "longid => logic",          Delimfix "CONST _"),
-    ("_context_const", typ "longid => aprop",          Delimfix "CONST _"),
-    ("_context_xconst", typ "id => logic",             Delimfix "XCONST _"),
-    ("_context_xconst", typ "id => aprop",             Delimfix "XCONST _"),
-    ("_context_xconst", typ "longid => logic",         Delimfix "XCONST _"),
-    ("_context_xconst", typ "longid => aprop",         Delimfix "XCONST _"),
+    ("_context_const", typ "id_position => logic",     Delimfix "CONST _"),
+    ("_context_const", typ "id_position => aprop",     Delimfix "CONST _"),
+    ("_context_const", typ "longid_position => logic", Delimfix "CONST _"),
+    ("_context_const", typ "longid_position => aprop", Delimfix "CONST _"),
+    ("_context_xconst", typ "id_position => logic",    Delimfix "XCONST _"),
+    ("_context_xconst", typ "id_position => aprop",    Delimfix "XCONST _"),
+    ("_context_xconst", typ "longid_position => logic", Delimfix "XCONST _"),
+    ("_context_xconst", typ "longid_position => aprop", Delimfix "XCONST _"),
     (const "==>",   typ "prop => prop => prop",        Delimfix "op ==>"),
     (const Term.dummy_patternN, typ "aprop",           Delimfix "'_"),
     ("_sort_constraint", typ "type => prop",           Delimfix "(1SORT'_CONSTRAINT/(1'(_')))"),
isabelle