equal
deleted
inserted
replaced
8 imports Main |
8 imports Main |
9 begin |
9 begin |
10 |
10 |
11 consts rewrite_HOLE :: "'a::{}" |
11 consts rewrite_HOLE :: "'a::{}" |
12 notation rewrite_HOLE ("HOLE") |
12 notation rewrite_HOLE ("HOLE") |
13 notation rewrite_HOLE ("\<box>") |
13 notation rewrite_HOLE ("\<hole>") |
14 |
14 |
15 lemma eta_expand: |
15 lemma eta_expand: |
16 fixes f :: "'a::{} \<Rightarrow> 'b::{}" |
16 fixes f :: "'a::{} \<Rightarrow> 'b::{}" |
17 shows "f \<equiv> \<lambda>x. f x" . |
17 shows "f \<equiv> \<lambda>x. f x" . |
18 |
18 |