src/Pure/Isar/isar_syn.ML
changeset 6972 3ae2eeabde80
parent 6953 b3f6c39aaa2e
child 7002 01a4e15ee253
equal deleted inserted replaced
6971:4a13e098ee86 6972:3ae2eeabde80
   308       >> (Toplevel.print oo (Toplevel.proof o IsarThy.presume)));
   308       >> (Toplevel.print oo (Toplevel.proof o IsarThy.presume)));
   309 
   309 
   310 val defP =
   310 val defP =
   311   OuterSyntax.command "def" "local definition" K.prf_asm
   311   OuterSyntax.command "def" "local definition" K.prf_asm
   312     ((P.opt_thm_name ":" -- (P.name -- Scan.option (P.$$$ "::" |-- P.typ) --
   312     ((P.opt_thm_name ":" -- (P.name -- Scan.option (P.$$$ "::" |-- P.typ) --
   313       (P.$$$ "=" |-- P.termp)) >> P.triple1) -- P.marg_comment
   313       (P.$$$ "==" |-- P.termp)) >> P.triple1) -- P.marg_comment
   314       >> (Toplevel.print oo (Toplevel.proof o IsarThy.local_def)));
   314       >> (Toplevel.print oo (Toplevel.proof o IsarThy.local_def)));
   315 
   315 
   316 val fixP =
   316 val fixP =
   317   OuterSyntax.command "fix" "fix variables (Skolem constants)" K.prf_asm
   317   OuterSyntax.command "fix" "fix variables (Skolem constants)" K.prf_asm
   318     (Scan.repeat1 (P.name -- Scan.option (P.$$$ "::" |-- P.typ)) -- P.marg_comment
   318     (Scan.repeat1 (P.name -- Scan.option (P.$$$ "::" |-- P.typ)) -- P.marg_comment