src/HOL/Refute.thy
changeset 46950 d0181abdbdac
parent 40178 00152d17855b
child 46960 f19e5837ad69
--- a/src/HOL/Refute.thy	Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/Refute.thy	Thu Mar 15 22:08:53 2012 +0100
@@ -9,6 +9,7 @@
 
 theory Refute
 imports Hilbert_Choice List Sledgehammer
+keywords "refute" :: diag and "refute_params" :: thy_decl
 uses "Tools/refute.ML"
 begin