diff options
Diffstat (limited to 'spartan/lib')
| -rw-r--r-- | spartan/lib/List.thy | 2 | ||||
| -rw-r--r-- | spartan/lib/Maybe.thy | 6 | ||||
| -rw-r--r-- | spartan/lib/Prelude.thy | 3 |
3 files changed, 6 insertions, 5 deletions
diff --git a/spartan/lib/List.thy b/spartan/lib/List.thy index dd51582..83e5149 100644 --- a/spartan/lib/List.thy +++ b/spartan/lib/List.thy @@ -149,7 +149,7 @@ Definition map: proof (elim xs) show "[]: List B" by intro next fix x ys - assume "x: A" "ys: List B" + assuming "x: A" "ys: List B" show "f x # ys: List B" by typechk qed diff --git a/spartan/lib/Maybe.thy b/spartan/lib/Maybe.thy index 0a7ec21..da22a4e 100644 --- a/spartan/lib/Maybe.thy +++ b/spartan/lib/Maybe.thy @@ -25,10 +25,10 @@ Definition MaybeInd: "\<And>a. a: A \<Longrightarrow> f a: C (some A a)" "m: Maybe A" shows "C m" - using assms[unfolded Maybe_def none_def some_def] + using assms[unfolded Maybe_def none_def some_def, type] apply (elim m) - apply (rule \<open>_ \<Longrightarrow> _: C (inl _ _ _)\<close>) - apply (elim, rule \<open>_: C (inr _ _ _)\<close>) + apply fact + apply (elim, fact) done Lemma Maybe_comp_none: 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 |