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 = transform_error (fn () => prove_goalw_cterm [] (cterm_of sign t') |
107 val thm = Tactic.prove sign [] [] t' (K (tac 1)); |
108 (fn ps => [cut_facts_tac ps 1, tac 1])) () |
|
109 in (ts, thm)::l end |
108 in (ts, thm)::l end |
110 handle ERROR_MESSAGE _ => l; |
109 handle ERROR_MESSAGE _ => l; |
111 |
110 |
112 |
111 |
113 (*** instantiation of adm_subst theorem (a bit tricky) ***) |
112 (*** instantiation of adm_subst theorem (a bit tricky) ***) |