diff -r 8ebdef196fd5 -r a031bcaf6719 IntEx.thy --- a/IntEx.thy Thu Nov 05 09:38:34 2009 +0100 +++ b/IntEx.thy Thu Nov 05 09:55:21 2009 +0100 @@ -158,7 +158,8 @@ ML {* val consts = lookup_quot_consts defs *} ML {* val t_a = atomize_thm @{thm ho_tst} *} -(*prove t_r: {* build_regularize_goal t_a rty rel @{context} *} +(* +prove t_r: {* build_regularize_goal t_a rty rel @{context} *} ML_prf {* fun tac ctxt = (ObjectLogic.full_atomize_tac) THEN' REPEAT_ALL_NEW (FIRST' [ @@ -183,6 +184,7 @@ val rt = build_repabs_term @{context} t_r consts rty qty val rg = Logic.mk_equals ((Thm.prop_of t_r), rt); *} +*) lemma foldl_rsp: "((IntEx.intrel ===> IntEx.intrel ===> IntEx.intrel) ===>