equal
deleted
inserted
replaced
444 |
444 |
445 lemma ttt3: "(\<lambda>x. ((op @) x ((op #) e []))) = (\<lambda>x. ((op #) e x))" |
445 lemma ttt3: "(\<lambda>x. ((op @) x ((op #) e []))) = (\<lambda>x. ((op #) e x))" |
446 sorry |
446 sorry |
447 |
447 |
448 lemma "(\<lambda>x. (FUNION x (INSERT e EMPTY))) = (\<lambda>x. (INSERT e x))" |
448 lemma "(\<lambda>x. (FUNION x (INSERT e EMPTY))) = (\<lambda>x. (INSERT e x))" |
449 apply (tactic {* procedure_tac @{context} @{thm ttt3} 1 *}) |
449 (* apply (tactic {* procedure_tac @{context} @{thm ttt3} 1 *}) *) |
450 sorry |
450 sorry |
451 |
451 |
452 end |
452 end |