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.
added longid syntax;
authorwenzelm
Fri, 10 Oct 1997 15:47:41 +0200
changeset 3829 d7333ef9e72c
parent 3828 f6a7ca242dc2
child 3830 7797327eca1d
added longid syntax;
src/Pure/Syntax/mixfix.ML file | annotate | diff | comparison | revisions
src/Pure/Syntax/type_ext.ML file | annotate | diff | comparison | revisions 
--- a/src/Pure/Syntax/mixfix.ML	Fri Oct 10 15:46:50 1997 +0200
+++ b/src/Pure/Syntax/mixfix.ML	Fri Oct 10 15:47:41 1997 +0200
@@ -172,6 +172,7 @@
   ("",             "pttrn => pttrns",               Delimfix "_"),
   ("_pttrns",      "[pttrn, pttrns] => pttrns",     Mixfix ("_/ _", [1, 0], 0)),
   ("",             "id => aprop",                   Delimfix "_"),
+  ("",             "longid => aprop",               Delimfix "_"),
   ("",             "var => aprop",                  Delimfix "_"),
   ("_aprop",       "aprop => prop",                 Delimfix "PROP _"),
   ("",             "prop => asms",                  Delimfix "_"),
@@ -182,6 +183,7 @@
   ("_mk_ofclassS", "_",                             NoSyn),
   ("_K",           "_",                             NoSyn),
   ("",             "id => logic",                   Delimfix "_"),
+  ("",             "longid => logic",               Delimfix "_"),
   ("",             "var => logic",                  Delimfix "_")];
 
 val pure_appl_syntax =
@@ -206,4 +208,5 @@
   ("==",       "['a::{}, 'a] => prop",  InfixrName ("\\<equiv>", 2)),
   ("!!",       "[idts, prop] => prop",  Mixfix ("(3\\<And>_./ _)", [0, 0], 0))];
 
+
 end;
--- a/src/Pure/Syntax/type_ext.ML	Fri Oct 10 15:46:50 1997 +0200
+++ b/src/Pure/Syntax/type_ext.ML	Fri Oct 10 15:47:41 1997 +0200
@@ -160,15 +160,21 @@
   [Mfix ("_",           tidT --> typeT,                "", [], max_pri),
    Mfix ("_",           tvarT --> typeT,               "", [], max_pri),
    Mfix ("_",           idT --> typeT,                 "", [], max_pri),
+   Mfix ("_",           longidT --> typeT,             "", [], max_pri),
    Mfix ("_::_",        [tidT, sortT] ---> typeT,      "_ofsort", [max_pri, 0], max_pri),
    Mfix ("_::_",        [tvarT, sortT] ---> typeT,     "_ofsort", [max_pri, 0], max_pri),
    Mfix ("_",           idT --> sortT,                 "", [], max_pri),
+   Mfix ("_",           longidT --> sortT,             "", [], max_pri),
    Mfix ("{}",          sortT,                         "_topsort", [], max_pri),
    Mfix ("{_}",         classesT --> sortT,            "_sort", [], max_pri),
    Mfix ("_",           idT --> classesT,              "", [], max_pri),
+   Mfix ("_",           longidT --> classesT,          "", [], max_pri),
    Mfix ("_,_",         [idT, classesT] ---> classesT, "_classes", [], max_pri),
+   Mfix ("_,_",         [longidT, classesT] ---> classesT, "_classes", [], max_pri),
    Mfix ("_ _",         [typeT, idT] ---> typeT,       "_tapp", [max_pri, 0], max_pri),
+   Mfix ("_ _",         [typeT, longidT] ---> typeT,   "_tapp", [max_pri, 0], max_pri),
    Mfix ("((1'(_,/ _'))_)", [typeT, typesT, idT] ---> typeT, "_tappl", [], max_pri),
+   Mfix ("((1'(_,/ _'))_)", [typeT, typesT, longidT] ---> typeT, "_tappl", [], max_pri),
    Mfix ("_",           typeT --> typesT,              "", [], max_pri),
    Mfix ("_,/ _",       [typeT, typesT] ---> typesT,   "_types", [], max_pri),
    Mfix ("(_/ => _)",   [typeT, typeT] ---> typeT,     "fun", [1, 0], 0),
isabelle