irrelevant reference to doubtful theory Code_Char
authorhaftmann
Mon, 29 Jan 2018 19:38:17 +0000
changeset 67526 a585c5b53576
parent 67525 5d04d7bcd5f6
child 67528 ea029c521b5b
irrelevant reference to doubtful theory Code_Char
src/Doc/Codegen/Computations.thy
--- a/src/Doc/Codegen/Computations.thy	Sun Jan 28 16:38:48 2018 +0000
+++ b/src/Doc/Codegen/Computations.thy	Mon Jan 29 19:38:17 2018 +0000
@@ -1,7 +1,6 @@
 theory Computations
   imports Codegen_Basics.Setup
     "HOL-Library.Code_Target_Int"
-    "HOL-Library.Code_Char"
 begin
 
 section \<open>Computations \label{sec:computations}\<close>