Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
compile
authorblanchet
Thu, 21 Nov 2013 21:33:34 +0100
changeset 54556 dd511ddcb203
parent 54555 e8c5e95d338b
child 54557 d71c2737ee21
compile
src/HOL/Library/Refute.thy file | annotate | diff | comparison | revisions
src/HOL/Library/refute.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Library/Refute.thy	Thu Nov 21 21:33:34 2013 +0100
+++ b/src/HOL/Library/Refute.thy	Thu Nov 21 21:33:34 2013 +0100
@@ -8,7 +8,7 @@
 header {* Refute *}
 
 theory Refute
-imports Hilbert_Choice List Sledgehammer
+imports Main
 keywords "refute" :: diag and "refute_params" :: thy_decl
 begin
 
--- a/src/HOL/Library/refute.ML	Thu Nov 21 21:33:34 2013 +0100
+++ b/src/HOL/Library/refute.ML	Thu Nov 21 21:33:34 2013 +0100
@@ -392,7 +392,7 @@
 (* TRANSLATION HOL -> PROPOSITIONAL LOGIC, BOOLEAN ASSIGNMENT -> MODEL       *)
 (* ------------------------------------------------------------------------- *)
 
-val typ_of_dtyp = ATP_Util.typ_of_dtyp
+val typ_of_dtyp = Nitpick_Util.typ_of_dtyp
 
 (* ------------------------------------------------------------------------- *)
 (* close_form: universal closure over schematic variables in 't'             *)
isabelle