diff options
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" |