src/Pure/Isar/isar_syn.ML
changeset 9589 95a66548c883
parent 9552 e3981c1f769d
child 9731 3eb72671e5db
--- a/src/Pure/Isar/isar_syn.ML	Mon Aug 14 14:50:32 2000 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Mon Aug 14 14:50:53 2000 +0200
@@ -195,6 +195,10 @@
   OuterSyntax.command "lemmas" "define lemmas" K.thy_decl
     (name_facts >> (Toplevel.theory o IsarThy.have_lemmas));
 
+val declareP =
+  OuterSyntax.improper_command "declare" "declare theorems (improper)" K.thy_script
+    (P.xthms1 -- P.marg_comment >> (Toplevel.theory o IsarThy.declare_theorems));
+
 
 (* name space entry path *)
 
@@ -670,8 +674,8 @@
   (*theory sections*)
   classesP, classrelP, defaultsortP, typedeclP, typeabbrP, nontermP,
   aritiesP, judgmentP, constsP, syntaxP, translationsP, axiomsP,
-  defsP, constdefsP, theoremsP, lemmasP, globalP, localP, hideP, useP,
-  mlP, ml_commandP, ml_setupP, setupP, method_setupP,
+  defsP, constdefsP, theoremsP, lemmasP, declareP, globalP, localP,
+  hideP, useP, mlP, ml_commandP, ml_setupP, setupP, method_setupP,
   parse_ast_translationP, parse_translationP, print_translationP,
   typed_print_translationP, print_ast_translationP,
   token_translationP, oracleP,