diff options
Diffstat (limited to 'spartan/lib/Prelude.thy')
| -rw-r--r-- | spartan/lib/Prelude.thy | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/spartan/lib/Prelude.thy b/spartan/lib/Prelude.thy index c0abf31..0043c1e 100644 --- a/spartan/lib/Prelude.thy +++ b/spartan/lib/Prelude.thy @@ -139,7 +139,7 @@ lemmas subsection \<open>Notation\<close> definition ifelse_i ("if _ then _ else _") - where [implicit]: "if x then a else b \<equiv> ifelse ? x a b" + where [implicit]: "if x then a else b \<equiv> ifelse {} x a b" translations "if x then a else b" \<leftharpoondown> "CONST ifelse C x a b" |