diff options
Diffstat (limited to 'spartan/lib/Prelude.thy')
| -rw-r--r-- | spartan/lib/Prelude.thy | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/spartan/lib/Prelude.thy b/spartan/lib/Prelude.thy index 6adbce8..c0abf31 100644 --- a/spartan/lib/Prelude.thy +++ b/spartan/lib/Prelude.thy @@ -105,7 +105,8 @@ Definition ifelse [rotated 1]: "a: C true" "b: C false" shows "C x" - by (elim x) (elim, rule *)+ + using assms[unfolded Bool_def true_def false_def, type] + by (elim x) (elim, fact)+ Lemma if_true: assumes |