equal
deleted
inserted
replaced
102 val contT = (T --> (fastype_of1 (T::parTs, t))) --> HOLogic.boolT; |
102 val contT = (T --> (fastype_of1 (T::parTs, t))) --> HOLogic.boolT; |
103 fun mk_all [] t = t |
103 fun mk_all [] t = t |
104 | mk_all ((a,T)::Ts) t = (all T) $ (Abs (a, T, mk_all Ts t)); |
104 | mk_all ((a,T)::Ts) t = (all T) $ (Abs (a, T, mk_all Ts t)); |
105 val t = HOLogic.mk_Trueprop((Const (cont_name, contT)) $ (Abs(s, T, t))); |
105 val t = HOLogic.mk_Trueprop((Const (cont_name, contT)) $ (Abs(s, T, t))); |
106 val t' = mk_all params (Logic.list_implies (prems, t)); |
106 val t' = mk_all params (Logic.list_implies (prems, t)); |
107 val thm = prove_goalw_cterm [] (cterm_of sign t') |
107 val thm = transform_error (fn () => prove_goalw_cterm [] (cterm_of sign t') |
108 (fn ps => [cut_facts_tac ps 1, tac 1]) |
108 (fn ps => [cut_facts_tac ps 1, tac 1])) () |
109 in (ts, thm)::l end |
109 in (ts, thm)::l end |
110 handle _ => l; |
110 handle ERROR_MESSAGE _ => l; |
111 |
111 |
112 |
112 |
113 (*** instantiation of adm_subst theorem (a bit tricky) ***) |
113 (*** instantiation of adm_subst theorem (a bit tricky) ***) |
114 |
114 |
115 fun inst_adm_subst_thm state i params s T subt t paths = |
115 fun inst_adm_subst_thm state i params s T subt t paths = |