| changeset 52990 | 6b6c4ec42024 |
| parent 51804 | be6e703908f4 |
| child 52992 | abd760a19e22 |
--- a/src/HOL/BNF/Examples/TreeFI.thy Mon Aug 12 21:30:37 2013 +0200 +++ b/src/HOL/BNF/Examples/TreeFI.thy Mon Aug 12 22:38:39 2013 +0200 @@ -20,7 +20,10 @@ lemma dtor[simp]: "treeFI_dtor tr = (lab tr, sub tr)" unfolding lab_def sub_def treeFI_case_def +(* by (metis fst_def pair_collapse snd_def) +*) +sorry definition pair_fun (infixr "\<odot>" 50) where "f \<odot> g \<equiv> \<lambda>x. (f x, g x)"