diff options
| author | Josh Chen | 2021-06-24 22:40:05 +0100 |
|---|---|---|
| committer | Josh Chen | 2021-06-24 22:40:05 +0100 |
| commit | f988d541364841cd208f4fd21ff8e5e2935fc7aa (patch) | |
| tree | 8ccc4d4e4cdde7572453ac0e250a224fe8db3da1 /mltt/lib/Prelude.thy | |
| parent | 0085798a86a35e2430a97289e894724f688db435 (diff) | |
Bad practice huge commit:
1. Rudimentary prototype definitional package
2. Started univalence
3. Various compatibility fixes and new theory stubs
4. Updated ROOT file
Diffstat (limited to 'mltt/lib/Prelude.thy')
| -rw-r--r-- | mltt/lib/Prelude.thy | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mltt/lib/Prelude.thy b/mltt/lib/Prelude.thy index 0393968..86165cd 100644 --- a/mltt/lib/Prelude.thy +++ b/mltt/lib/Prelude.thy @@ -100,7 +100,7 @@ Lemma unfolding Bool_def true_def false_def by typechk+ \<comment> \<open>Definitions like these should be handled by a future function package\<close> -Definition ifelse [rotated 1]: +Lemma (def) ifelse [rotated 1]: assumes *[unfolded Bool_def true_def false_def]: "\<And>x. x: Bool \<Longrightarrow> C x: U i" "x: Bool" |