diff --git a/library/standard/logic/axioms/default.lean b/library/standard/logic/axioms/default.lean
new file mode 100644
index 0000000000..0c549c5059
--- /dev/null
+++ b/library/standard/logic/axioms/default.lean
@@ -0,0 +1,8 @@
+----------------------------------------------------------------------------------------------------
+--- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+--- Released under Apache 2.0 license as described in the file LICENSE.
+--- Author: Jeremy Avigad
+----------------------------------------------------------------------------------------------------
+
+import logic.axioms.classical logic.axioms.funext logic.axioms.hilbert logic.axioms.piext
+import logic.axioms.prop_decidable
\ No newline at end of file
diff --git a/library/standard/logic/axioms/hilbert.lean b/library/standard/logic/axioms/hilbert.lean
index 457e08f39b..f45e15c000 100644
--- a/library/standard/logic/axioms/hilbert.lean
+++ b/library/standard/logic/axioms/hilbert.lean
@@ -1,4 +1,5 @@
------------------------------------------------------------------------------------------------------- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+----------------------------------------------------------------------------------------------------
+-- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
 ----------------------------------------------------------------------------------------------------