# HG changeset patch # User blanchet # Date 1402585323 -7200 # Node ID 25aff3b8d550098c4c867a64b9b18e4980e1f0f7 # Parent 7fca4159117f4ca5155352de89c2518a18778eb8 tuned dependencies diff -r 7fca4159117f -r 25aff3b8d550 src/HOL/Nitpick.thy --- a/src/HOL/Nitpick.thy Thu Jun 12 17:02:03 2014 +0200 +++ b/src/HOL/Nitpick.thy Thu Jun 12 17:02:03 2014 +0200 @@ -8,7 +8,7 @@ header {* Nitpick: Yet Another Counterexample Generator for Isabelle/HOL *} theory Nitpick -imports BNF_FP_Base Map Record +imports Record keywords "nitpick" :: diag and "nitpick_params" :: thy_decl diff -r 7fca4159117f -r 25aff3b8d550 src/HOL/Random.thy --- a/src/HOL/Random.thy Thu Jun 12 17:02:03 2014 +0200 +++ b/src/HOL/Random.thy Thu Jun 12 17:02:03 2014 +0200 @@ -4,7 +4,7 @@ header {* A HOL random engine *} theory Random -imports Code_Numeral List +imports List begin notation fcomp (infixl "\>" 60) diff -r 7fca4159117f -r 25aff3b8d550 src/HOL/Sledgehammer.thy --- a/src/HOL/Sledgehammer.thy Thu Jun 12 17:02:03 2014 +0200 +++ b/src/HOL/Sledgehammer.thy Thu Jun 12 17:02:03 2014 +0200 @@ -7,7 +7,7 @@ header {* Sledgehammer: Isabelle--ATP Linkup *} theory Sledgehammer -imports Presburger ATP SMT2 +imports Presburger SMT2 keywords "sledgehammer" :: diag and "sledgehammer_params" :: thy_decl begin