classified show/thus as prf_asm_goal, which is usually hilited in PG;
authorwenzelm
Tue Dec 12 20:49:27 2006 +0100 (2006-12-12 ago)
changeset 218006035bfcd72d8
parent 21799 a85e3bbc76fb
child 21801 c77bc21b3eef
classified show/thus as prf_asm_goal, which is usually hilited in PG;
src/Pure/Isar/isar_syn.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Dec 12 20:49:26 2006 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Dec 12 20:49:27 2006 +0100
     1.3 @@ -372,7 +372,7 @@
     1.4          -- P.opt_begin
     1.5        >> (fn (((is_open, name), (expr, elems)), begin) =>
     1.6            Toplevel.begin_local_theory begin
     1.7 -            (Locale.add_locale is_open name expr elems #-> TheoryTarget.begin)));
     1.8 +            (Locale.add_locale is_open name expr elems #-> TheoryTarget.begin false)));
     1.9  
    1.10  val interpretationP =
    1.11    OuterSyntax.command "interpretation"
    1.12 @@ -420,12 +420,12 @@
    1.13  
    1.14  val showP =
    1.15    OuterSyntax.command "show" "state local goal, solving current obligation"
    1.16 -    (K.tag_proof K.prf_goal)
    1.17 +    (K.tag_proof K.prf_asm_goal)
    1.18      (P.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.show));
    1.19  
    1.20  val thusP =
    1.21    OuterSyntax.command "thus" "abbreviates \"then show\""
    1.22 -    (K.tag_proof K.prf_goal)
    1.23 +    (K.tag_proof K.prf_asm_goal)
    1.24      (P.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.thus));
    1.25  
    1.26