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.
agree on keyword categories with ML;
authorwenzelm
Fri, 01 Aug 2014 20:20:17 +0200
changeset 57836 7944e2588d1c
parent 57835 43ff8638c02c
child 57837 63e3c45b85e1
agree on keyword categories with ML;
src/Pure/Isar/keyword.scala file | annotate | diff | comparison | revisions 
--- a/src/Pure/Isar/keyword.scala	Fri Aug 01 20:15:00 2014 +0200
+++ b/src/Pure/Isar/keyword.scala	Fri Aug 01 20:20:17 2014 +0200
@@ -52,7 +52,7 @@
 
   val theory =
     Set(THY_BEGIN, THY_END, THY_HEADING1, THY_HEADING2, THY_HEADING3, THY_HEADING4,
-      THY_DECL, THY_GOAL)
+      THY_LOAD, THY_DECL, THY_GOAL)
   val theory1 = Set(THY_BEGIN, THY_END)
   val theory2 = Set(THY_DECL, THY_GOAL)
   val theory_body =
@@ -60,8 +60,8 @@
 
   val proof =
     Set(QED, QED_SCRIPT, QED_BLOCK, QED_GLOBAL, PRF_HEADING2, PRF_HEADING3, PRF_HEADING4,
-      PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CHAIN, PRF_DECL, PRF_ASM, PRF_ASM_GOAL,
-      PRF_ASM_GOAL_SCRIPT, PRF_SCRIPT)
+      PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE, PRF_CHAIN, PRF_DECL,
+      PRF_ASM, PRF_ASM_GOAL, PRF_ASM_GOAL_SCRIPT, PRF_SCRIPT)
   val proof1 =
     Set(QED, QED_SCRIPT, QED_BLOCK, QED_GLOBAL, PRF_GOAL, PRF_BLOCK, PRF_OPEN, PRF_CLOSE,
       PRF_CHAIN, PRF_DECL)
isabelle