diff options
| author | Josh Chen | 2018-08-07 18:06:10 +0200 |
|---|---|---|
| committer | Josh Chen | 2018-08-07 18:06:10 +0200 |
| commit | ec8e1d9d245950f185f6d4ff1b5e1b8755e7202c (patch) | |
| tree | 2c7515ddb206223a71cb35ab06b8080c71338159 /scratch.thy | |
| parent | dc2730916482bd230f9bd5244b8b2cc9d005f69a (diff) | |
Tweaks
Diffstat (limited to '')
| -rw-r--r-- | scratch.thy | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/scratch.thy b/scratch.thy index 55e7023..e06fb7e 100644 --- a/scratch.thy +++ b/scratch.thy @@ -3,6 +3,12 @@ theory scratch begin +lemma + assumes "\<Sum>x:A. B(x): U(i)" "(a,b): \<Sum>x:A. B(x)" + shows "a : A" +proof (rule Sum_form_conds) + + abbreviation pred where "pred \<equiv> \<^bold>\<lambda>n:\<nat>. ind\<^sub>\<nat>(\<lambda>n c. n, 0, n)" schematic_goal "?a: (pred`0) =\<^sub>\<nat> 0" |