Raw File
default.lean
/-
Copyright (c) E.W.Ayers. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.

Author: E.W.Ayers
-/
prelude
import init.meta.widget.basic
import init.meta.widget.interactive_expr
import init.meta.widget.tactic_component
import init.meta.widget.html_cmd
import init.meta.widget.replace_save_info
back to top