--- a/src/HOL/Inductive.thy Thu Mar 15 17:45:54 2012 +0100 +++ b/src/HOL/Inductive.thy Thu Mar 15 19:02:34 2012 +0100 @@ -6,6 +6,7 @@ theory Inductive imports Complete_Lattices +keywords "monos" uses "Tools/dseq.ML" ("Tools/inductive.ML")