src/HOL/Tools/refute_isar.ML
changeset 24867 e5b55d7be9bb
parent 22092 ab3dfcef6489
child 26000 b629b4f2026c
     1.1 --- a/src/HOL/Tools/refute_isar.ML	Sat Oct 06 16:41:22 2007 +0200
     1.2 +++ b/src/HOL/Tools/refute_isar.ML	Sat Oct 06 16:50:04 2007 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  syntax.
     1.5  *)
     1.6  
     1.7 -structure RefuteIsar =
     1.8 +structure RefuteIsar: sig end =
     1.9  struct
    1.10  
    1.11  (* ------------------------------------------------------------------------- *)
    1.12 @@ -56,7 +56,7 @@
    1.13  
    1.14  	fun refute_parser tokens = (refute_scan_args tokens) |>> refute_trans;
    1.15  
    1.16 -	val refute_cmd = OuterSyntax.improper_command "refute"
    1.17 +	val _ = OuterSyntax.improper_command "refute"
    1.18  		"try to find a model that refutes a given subgoal"
    1.19  		OuterKeyword.diag refute_parser;
    1.20  
    1.21 @@ -101,15 +101,9 @@
    1.22  	fun refute_params_parser tokens =
    1.23  		(refute_params_scan_args tokens) |>> refute_params_trans;
    1.24  
    1.25 -	val refute_params_cmd = OuterSyntax.command "refute_params"
    1.26 +	val _ = OuterSyntax.command "refute_params"
    1.27  		"show/store default parameters for the 'refute' command"
    1.28  		OuterKeyword.thy_decl refute_params_parser;
    1.29  
    1.30  end;
    1.31  
    1.32 -(* ------------------------------------------------------------------------- *)
    1.33 -(* add the two new commands 'refute' and 'refute_params' to Isabelle/Isar's  *)
    1.34 -(* outer syntax                                                              *)
    1.35 -(* ------------------------------------------------------------------------- *)
    1.36 -
    1.37 -OuterSyntax.add_parsers [RefuteIsar.refute_cmd, RefuteIsar.refute_params_cmd];