src/Pure/Isar/isar_syn.ML
changeset 9776 a126bc3b7376
parent 9731 3eb72671e5db
child 9978 d4af3f6fa997
equal deleted inserted replaced
9775:da698a96c4f3 9776:a126bc3b7376
   195 val lemmasP =
   195 val lemmasP =
   196   OuterSyntax.command "lemmas" "define lemmas" K.thy_decl
   196   OuterSyntax.command "lemmas" "define lemmas" K.thy_decl
   197     (name_facts >> (Toplevel.theory o IsarThy.have_lemmas));
   197     (name_facts >> (Toplevel.theory o IsarThy.have_lemmas));
   198 
   198 
   199 val declareP =
   199 val declareP =
   200   OuterSyntax.improper_command "declare" "declare theorems (improper)" K.thy_script
   200   OuterSyntax.command "declare" "declare theorems (improper)" K.thy_script
   201     (P.xthms1 -- P.marg_comment >> (Toplevel.theory o IsarThy.declare_theorems));
   201     (P.xthms1 -- P.marg_comment >> (Toplevel.theory o IsarThy.declare_theorems));
   202 
   202 
   203 
   203 
   204 (* name space entry path *)
   204 (* name space entry path *)
   205 
   205