diff options
| author | Josh Chen | 2019-02-10 03:16:51 +0100 |
|---|---|---|
| committer | Josh Chen | 2019-02-10 03:16:51 +0100 |
| commit | 29068d381a8b5d95c7fd4dc6111dcfb3a181f0bd (patch) | |
| tree | 33e6c5614f7bd29bf0e66292b3122b5d414c7a7d /HoTT_Base.thy | |
| parent | afef9e63cb11267dc69b714a8b76415d75e2dd37 (diff) | |
Explicit references in antiquotations in typing.ML. Move trace switch definition to HoTT_Base.
Diffstat (limited to 'HoTT_Base.thy')
| -rw-r--r-- | HoTT_Base.thy | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/HoTT_Base.thy b/HoTT_Base.thy index ed8c18b..23e51e5 100644 --- a/HoTT_Base.thy +++ b/HoTT_Base.thy @@ -27,6 +27,9 @@ section \<open>Setup non-core logic functionality\<close> declare[[eta_contract=false]] \<comment> \<open>Do not eta-contract\<close> +ML \<open>val trace = Attrib.setup_config_bool @{binding "trace"} (K false)\<close> + \<comment> \<open>Context attribute for tracing; use declare[[trace=true]] at any point in a theory to turn on.\<close> + text \<open>The following file sets up type assumption and inference functionality.\<close> ML_file "typing.ML" |