# HG changeset patch # User Cezary Kaliszyk # Date 1260287811 -3600 # Node ID 793c3ff4bc2ab25d6d6834d6d83c117023ee30bd # Parent 54573efed52767c89228602bc1d27d207a03152a# Parent 2e51e13158391de70d0fdd0be5a811da1a90a3d5 merge diff -r 2e51e1315839 -r 793c3ff4bc2a Quot/Examples/FSet.thy --- a/Quot/Examples/FSet.thy Tue Dec 08 16:36:01 2009 +0100 +++ b/Quot/Examples/FSet.thy Tue Dec 08 16:56:51 2009 +0100 @@ -434,11 +434,14 @@ lemma "(\e. (FUNION x (INSERT e EMPTY))) = (\e. (INSERT e x))" apply (tactic {* procedure_tac @{context} @{thm ttt2} 1 *}) apply(tactic {* regularize_tac @{context} 1 *}) -defer +apply(rule impI) +apply(simp) +apply(rule allI) +apply(rule list_eq_refl) apply(tactic {* all_inj_repabs_tac @{context} 1*}) apply(tactic {* clean_tac @{context} 1 *}) apply(tactic {* clean_tac @{context} 1 *}) (* TODO: needs lambda_prs twice *) -sorry +done lemma ttt3: "(\x. ((op @) x ((op #) e []))) = (\x. ((op #) e x))" sorry