diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 81617319f..99f5cb619 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -226,7 +226,7 @@ endif()
 set(CMAKE_EXE_LINKER_FLAGS_TESTCOV "${CMAKE_EXE_LINKER_FLAGS} -fprofile-arcs -ftest-coverage")
 set(EXTRA_LIBS ${LEAN_LIBS} ${EXTRA_LIBS})
 add_subdirectory(shell)
-add_subdirectory(extra)
+add_subdirectory(builtin)
 
 add_subdirectory(tests/util)
 add_subdirectory(tests/util/numerics)
diff --git a/src/builtin/CMakeLists.txt b/src/builtin/CMakeLists.txt
new file mode 100644
index 000000000..ec5fb4a3b
--- /dev/null
+++ b/src/builtin/CMakeLists.txt
@@ -0,0 +1,26 @@
+add_library(builtin builtin.cpp)
+
+file(GLOB LEANLIB "${LEAN_SOURCE_DIR}/builtin/*.lean")
+FOREACH(FILE ${LEANLIB})
+  get_filename_component(BASENAME ${FILE} NAME_WE)
+  set(FNAME "${BASENAME}.olean")
+  add_custom_command(OUTPUT ${LEAN_BINARY_DIR}/builtin/${FNAME}
+    COMMAND ${LEAN_BINARY_DIR}/shell/lean -o ${LEAN_BINARY_DIR}/builtin/${FNAME} ${FILE}
+    COMMAND ${CMAKE_COMMAND} -E copy ${LEAN_BINARY_DIR}/builtin/${FNAME} ${LEAN_BINARY_DIR}/shell/${FNAME}
+    DEPENDS ${FILE} ${LEAN_BINARY_DIR}/shell/lean)
+  add_custom_target(${FNAME}_builtin DEPENDS ${LEAN_BINARY_DIR}/builtin/${FNAME})
+  add_dependencies(builtin ${FNAME}_builtin)
+  install(FILES ${LEAN_BINARY_DIR}/builtin/${FNAME} DESTINATION library)
+ENDFOREACH(FILE)
+
+file(GLOB LEANLIB "${LEAN_SOURCE_DIR}/builtin/*.lua")
+FOREACH(FILE ${LEANLIB})
+  get_filename_component(FNAME ${FILE} NAME)
+  add_custom_command(OUTPUT ${LEAN_BINARY_DIR}/builtin/${FNAME}
+    COMMAND ${CMAKE_COMMAND} -E copy ${FILE} ${LEAN_BINARY_DIR}/builtin/${FNAME}
+    COMMAND ${CMAKE_COMMAND} -E copy ${FILE} ${LEAN_BINARY_DIR}/shell/${FNAME}
+    DEPENDS ${FILE})
+  add_custom_target("${FNAME}_builtin" DEPENDS ${LEAN_BINARY_DIR}/builtin/${FNAME})
+  add_dependencies(builtin "${FNAME}_builtin")
+  install(FILES ${LEAN_BINARY_DIR}/builtin/${FNAME} DESTINATION library)
+ENDFOREACH(FILE)
diff --git a/src/builtin/README.md b/src/builtin/README.md
new file mode 100644
index 000000000..85c85ce2d
--- /dev/null
+++ b/src/builtin/README.md
@@ -0,0 +1,4 @@
+Extra functionality
+-------------------
+
+This directory contains Lean theories and additional Lua scripts.
diff --git a/src/extra/extra.cpp b/src/builtin/builtin.cpp
similarity index 100%
rename from src/extra/extra.cpp
rename to src/builtin/builtin.cpp
diff --git a/src/extra/cast.lean b/src/builtin/cast.lean
similarity index 100%
rename from src/extra/cast.lean
rename to src/builtin/cast.lean
diff --git a/src/extra/find.lua b/src/builtin/find.lua
similarity index 100%
rename from src/extra/find.lua
rename to src/builtin/find.lua
diff --git a/src/extra/macros.lua b/src/builtin/macros.lua
similarity index 100%
rename from src/extra/macros.lua
rename to src/builtin/macros.lua
diff --git a/src/extra/tactic.lua b/src/builtin/tactic.lua
similarity index 100%
rename from src/extra/tactic.lua
rename to src/builtin/tactic.lua
diff --git a/src/extra/template.lua b/src/builtin/template.lua
similarity index 100%
rename from src/extra/template.lua
rename to src/builtin/template.lua
diff --git a/src/extra/util.lua b/src/builtin/util.lua
similarity index 100%
rename from src/extra/util.lua
rename to src/builtin/util.lua
diff --git a/src/extra/CMakeLists.txt b/src/extra/CMakeLists.txt
deleted file mode 100644
index 668fe43b7..000000000
--- a/src/extra/CMakeLists.txt
+++ /dev/null
@@ -1,26 +0,0 @@
-add_library(extra extra.cpp)
-
-file(GLOB LEANLIB "${LEAN_SOURCE_DIR}/extra/*.lean")
-FOREACH(FILE ${LEANLIB})
-  get_filename_component(BASENAME ${FILE} NAME_WE)
-  set(FNAME "${BASENAME}.olean")
-  add_custom_command(OUTPUT ${LEAN_BINARY_DIR}/extra/${FNAME}
-    COMMAND ${LEAN_BINARY_DIR}/shell/lean -o ${LEAN_BINARY_DIR}/extra/${FNAME} ${FILE}
-    COMMAND ${CMAKE_COMMAND} -E copy ${LEAN_BINARY_DIR}/extra/${FNAME} ${LEAN_BINARY_DIR}/shell/${FNAME}
-    DEPENDS ${FILE} ${LEAN_BINARY_DIR}/shell/lean)
-  add_custom_target(${FNAME}_extra DEPENDS ${LEAN_BINARY_DIR}/extra/${FNAME})
-  add_dependencies(extra ${FNAME}_extra)
-  install(FILES ${LEAN_BINARY_DIR}/extra/${FNAME} DESTINATION library)
-ENDFOREACH(FILE)
-
-file(GLOB LEANLIB "${LEAN_SOURCE_DIR}/extra/*.lua")
-FOREACH(FILE ${LEANLIB})
-  get_filename_component(FNAME ${FILE} NAME)
-  add_custom_command(OUTPUT ${LEAN_BINARY_DIR}/extra/${FNAME}
-    COMMAND ${CMAKE_COMMAND} -E copy ${FILE} ${LEAN_BINARY_DIR}/extra/${FNAME}
-    COMMAND ${CMAKE_COMMAND} -E copy ${FILE} ${LEAN_BINARY_DIR}/shell/${FNAME}
-    DEPENDS ${FILE})
-  add_custom_target("${FNAME}_extra" DEPENDS ${LEAN_BINARY_DIR}/extra/${FNAME})
-  add_dependencies(extra "${FNAME}_extra")
-  install(FILES ${LEAN_BINARY_DIR}/extra/${FNAME} DESTINATION library)
-ENDFOREACH(FILE)
diff --git a/src/extra/README.md b/src/extra/README.md
deleted file mode 100644
index bdc72073e..000000000
--- a/src/extra/README.md
+++ /dev/null
@@ -1,5 +0,0 @@
-Extra functionality
--------------------
-
-This directory contains several Lua scripts that provide additional
-functionality to Lean.