1.1 --- a/src/Provers/classical.ML	Sun Jul 23 11:59:21 2000 +0200
     1.2 +++ b/src/Provers/classical.ML	Sun Jul 23 12:01:05 2000 +0200
     1.3 @@ -327,17 +327,17 @@
     1.4    is still allowed.*)
     1.5  fun warn_dup th (CS{safeIs, safeEs, hazIs, hazEs, xtraIs, xtraEs, ...}) = 
     1.6         if mem_thm (th, safeIs) then 
     1.7 -	 warning ("Rule already declared as safe introduction (intro)\n" ^ string_of_thm th)
     1.8 +	 warning ("Rule already declared as safe introduction (intro!)\n" ^ string_of_thm th)
     1.9    else if mem_thm (th, safeEs) then
    1.10 -         warning ("Rule already declared as safe elimination (elim)\n" ^ string_of_thm th)
    1.11 +         warning ("Rule already declared as safe elimination (elim!)\n" ^ string_of_thm th)
    1.12    else if mem_thm (th, hazIs) then 
    1.13 -         warning ("Rule already declared as unsafe introduction (intro?)\n" ^ string_of_thm th)
    1.14 +         warning ("Rule already declared as unsafe introduction (intro)\n" ^ string_of_thm th)
    1.15    else if mem_thm (th, hazEs) then 
    1.16 -         warning ("Rule already declared as unsafe elimination (elim?)\n" ^ string_of_thm th)
    1.17 +         warning ("Rule already declared as unsafe elimination (elim)\n" ^ string_of_thm th)
    1.18    else if mem_thm (th, xtraIs) then 
    1.19 -         warning ("Rule already declared as extra introduction (intro??)\n" ^ string_of_thm th)
    1.20 +         warning ("Rule already declared as extra introduction (intro?)\n" ^ string_of_thm th)
    1.21    else if mem_thm (th, xtraEs) then 
    1.22 -         warning ("Rule already declared as extra elimination (elim??)\n" ^ string_of_thm th)
    1.23 +         warning ("Rule already declared as extra elimination (elim?)\n" ^ string_of_thm th)
    1.24    else ();
    1.25  
    1.26  (*** Safe rules ***)
    1.27 @@ -1030,12 +1030,12 @@
    1.28  
    1.29  val colon = Args.$$$ ":";
    1.30  val query = Args.$$$ "?";
    1.31 -val qquery = Args.$$$ "??";
    1.32 +val bang = Args.$$$ "!";
    1.33  val query_colon = Args.$$$ "?:";
    1.34 -val qquery_colon = Args.$$$ "??:";
    1.35 +val bang_colon = Args.$$$ "!:";
    1.36  
    1.37  fun cla_att change xtra haz safe = Attrib.syntax
    1.38 -  (Scan.lift ((qquery >> K xtra || query >> K haz || Scan.succeed safe) >> change));
    1.39 +  (Scan.lift ((query >> K xtra || bang >> K haz || Scan.succeed safe) >> change));
    1.40  
    1.41  fun cla_attr f g h = (cla_att change_global_cs f g h, cla_att change_local_cs f g h);
    1.42  val del_attr = (Attrib.no_args delrule_global, Attrib.no_args delrule_local);
    1.43 @@ -1146,14 +1146,14 @@
    1.44  (* automatic methods *)
    1.45  
    1.46  val cla_modifiers =
    1.47 - [Args.$$$ destN -- qquery_colon >> K ((I, xtra_dest_local):Method.modifier),
    1.48 -  Args.$$$ destN -- query_colon >> K (I, haz_dest_local),
    1.49 + [Args.$$$ destN -- query_colon >> K ((I, xtra_dest_local):Method.modifier),
    1.50 +  Args.$$$ destN -- bang_colon >> K (I, haz_dest_local),
    1.51    Args.$$$ destN -- colon >> K (I, safe_dest_local),
    1.52 -  Args.$$$ elimN -- qquery_colon >> K (I, xtra_elim_local),
    1.53 -  Args.$$$ elimN -- query_colon >> K (I, haz_elim_local),
    1.54 +  Args.$$$ elimN -- query_colon >> K (I, xtra_elim_local),
    1.55 +  Args.$$$ elimN -- bang_colon >> K (I, haz_elim_local),
    1.56    Args.$$$ elimN -- colon >> K (I, safe_elim_local),
    1.57 -  Args.$$$ introN -- qquery_colon >> K (I, xtra_intro_local),
    1.58 -  Args.$$$ introN -- query_colon >> K (I, haz_intro_local),
    1.59 +  Args.$$$ introN -- query_colon >> K (I, xtra_intro_local),
    1.60 +  Args.$$$ introN -- bang_colon >> K (I, haz_intro_local),
    1.61    Args.$$$ introN -- colon >> K (I, safe_intro_local),
    1.62    Args.$$$ delN -- colon >> K (I, delrule_local)];
    1.63