Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Proofs/Extraction/Higman_Extraction.thy
changeset 67320 6afba546f0e5
parent 66453 cc19f7ca2ed6
child 67399 eab6ce8368fa 
--- a/src/HOL/Proofs/Extraction/Higman_Extraction.thy	Tue Jan 02 16:17:13 2018 +0100
+++ b/src/HOL/Proofs/Extraction/Higman_Extraction.thy	Tue Jan 02 16:40:54 2018 +0100
@@ -6,7 +6,7 @@
 subsection \<open>Extracting the program\<close>
 
 theory Higman_Extraction
-imports Higman "HOL-Library.Old_Datatype" "HOL-Library.Open_State_Syntax"
+imports Higman "HOL-Library.Realizers" "HOL-Library.Open_State_Syntax"
 begin
 
 declare R.induct [ind_realizer]
isabelle