fix, assume, presume: prf_asm;
authorwenzelm
Thu Jul 01 17:24:29 1999 +0200 (1999-07-01 ago)
changeset 6869850812ed9976
parent 6868 27ba88d57399
child 6870 43d64c520d11
fix, assume, presume: prf_asm;
src/Pure/Isar/isar_syn.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Thu Jul 01 17:24:14 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Thu Jul 01 17:24:29 1999 +0200
     1.3 @@ -288,17 +288,17 @@
     1.4  (* proof context *)
     1.5  
     1.6  val assumeP =
     1.7 -  OuterSyntax.command "assume" "assume propositions" K.prf_decl
     1.8 +  OuterSyntax.command "assume" "assume propositions" K.prf_asm
     1.9      ((P.opt_thm_name ":" -- Scan.repeat1 propp >> P.triple1) -- P.marg_comment
    1.10        >> (Toplevel.print oo (Toplevel.proof o IsarThy.assume)));
    1.11  
    1.12  val presumeP =
    1.13 -  OuterSyntax.command "presume" "assume propositions, to be established later" K.prf_decl
    1.14 +  OuterSyntax.command "presume" "assume propositions, to be established later" K.prf_asm
    1.15      ((P.opt_thm_name ":" -- Scan.repeat1 propp >> P.triple1) -- P.marg_comment
    1.16        >> (Toplevel.print oo (Toplevel.proof o IsarThy.presume)));
    1.17  
    1.18  val fixP =
    1.19 -  OuterSyntax.command "fix" "fix variables (Skolem constants)" K.prf_decl
    1.20 +  OuterSyntax.command "fix" "fix variables (Skolem constants)" K.prf_asm
    1.21      (Scan.repeat1 (P.name -- Scan.option (P.$$$ "::" |-- P.typ)) -- P.marg_comment
    1.22        >> (Toplevel.print oo (Toplevel.proof o IsarThy.fix)));
    1.23