diff options
| author | Josh Chen | 2019-02-17 18:34:38 +0100 |
|---|---|---|
| committer | Josh Chen | 2019-02-17 18:34:38 +0100 |
| commit | 68aa069172933b875d70a5ef71e9db0ae685a92d (patch) | |
| tree | bd1da2111e12bab878641661d91f95f66f8132cc /Projections.thy | |
| parent | 76b57317d7568f4dcd673b1b8085601c6c723355 (diff) | |
Method "quantify" converts product inhabitation into Pure universal statements. Also misc. cleanups.
Diffstat (limited to 'Projections.thy')
| -rw-r--r-- | Projections.thy | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Projections.thy b/Projections.thy index c819240..8ff6b30 100644 --- a/Projections.thy +++ b/Projections.thy @@ -39,7 +39,7 @@ lemma snd_cmp: assumes "A: U i" and "B: A \<leadsto> U i" and "a: A" and "b: B a" shows "snd A B <a,b> \<equiv> b" unfolding snd_def by (derive lems: assms) -lemmas Proj_types [intro] = fst_type snd_type -lemmas Proj_comps [comp] = fst_cmp snd_cmp +lemmas Proj_type [intro] = fst_type snd_type +lemmas Proj_comp [comp] = fst_cmp snd_cmp end |