diff options
| author | Josh Chen | 2019-02-23 18:58:20 +0100 |
|---|---|---|
| committer | Josh Chen | 2019-02-23 18:58:20 +0100 |
| commit | 76a009527d42c9939575f429a406a084c48fe653 (patch) | |
| tree | b047e7e64af6e3c61b7f149031bbe78695a6137b /Projections.thy | |
| parent | 232856fbef15105f619a5c1056da2602984804df (diff) | |
touchups
Diffstat (limited to 'Projections.thy')
| -rw-r--r-- | Projections.thy | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Projections.thy b/Projections.thy index 8ff6b30..1473e08 100644 --- a/Projections.thy +++ b/Projections.thy @@ -21,7 +21,7 @@ declare fst_type [intro] lemma fst_cmp: assumes "A: U i" and "B: A \<leadsto> U i" and "a: A" and "b: B a" shows "fst A <a, b> \<equiv> a" -unfolding fst_def by compute (derive lems: assms) +unfolding fst_def by (subst comp) (derive lems: assms) declare fst_cmp [comp] |