# HG changeset patch
# User wenzelm
# Date 966257453 -7200
# Node ID 95a66548c8837a02b7bbea62ddbb168846b561de
# Parent  96059cbcb0eb12fd10c7437a6501a05f192114b6
added "declare" command;

diff -r 96059cbcb0eb -r 95a66548c883 src/Pure/Isar/isar_syn.ML
--- 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,