equal
deleted
inserted
replaced
17 infix 1 ===; infix 1 ~= ; infix 1 <<; infix 1 ~<<; |
17 infix 1 ===; infix 1 ~= ; infix 1 <<; infix 1 ~<<; |
18 infix 9 ` ; infix 9 `% ; infix 9 `%%; infixr 9 oo; |
18 infix 9 ` ; infix 9 `% ; infix 9 `%%; infixr 9 oo; |
19 |
19 |
20 (* ----- general proof facilities ------------------------------------------- *) |
20 (* ----- general proof facilities ------------------------------------------- *) |
21 |
21 |
|
22 (* FIXME better avoid this low-level stuff *) |
22 fun inferT sg pre_tm = |
23 fun inferT sg pre_tm = |
23 #1 (Sign.infer_types (Sign.pp sg) sg (K NONE) (K NONE) [] true ([pre_tm],propT)); |
24 #1 (Sign.infer_types (Sign.pp sg) sg (Sign.consts_of sg) (K NONE) (K NONE) [] true ([pre_tm],propT)); |
24 |
25 |
25 fun pg'' thy defs t tacs = |
26 fun pg'' thy defs t tacs = |
26 let val t' = inferT thy t in |
27 let val t' = inferT thy t in |
27 standard (Goal.prove thy [] (Logic.strip_imp_prems t') (Logic.strip_imp_concl t') |
28 standard (Goal.prove thy [] (Logic.strip_imp_prems t') (Logic.strip_imp_concl t') |
28 (fn prems => rewrite_goals_tac defs THEN EVERY (tacs (map (rewrite_rule defs) prems)))) |
29 (fn prems => rewrite_goals_tac defs THEN EVERY (tacs (map (rewrite_rule defs) prems)))) |