equal
deleted
inserted
replaced
16 val fixed_judgment: Sign.sg -> string -> term |
16 val fixed_judgment: Sign.sg -> string -> term |
17 val assert_propT: Sign.sg -> term -> term |
17 val assert_propT: Sign.sg -> term -> term |
18 val declare_atomize: theory attribute |
18 val declare_atomize: theory attribute |
19 val declare_rulify: theory attribute |
19 val declare_rulify: theory attribute |
20 val atomize_term: Sign.sg -> term -> term |
20 val atomize_term: Sign.sg -> term -> term |
|
21 val atomize_thm: thm -> thm |
21 val atomize_rule: Sign.sg -> cterm -> thm |
22 val atomize_rule: Sign.sg -> cterm -> thm |
22 val atomize_tac: int -> tactic |
23 val atomize_tac: int -> tactic |
23 val full_atomize_tac: int -> tactic |
24 val full_atomize_tac: int -> tactic |
24 val atomize_goal: int -> thm -> thm |
25 val atomize_goal: int -> thm -> thm |
25 val rulify: thm -> thm |
26 val rulify: thm -> thm |
151 fun atomize_term sg = |
152 fun atomize_term sg = |
152 drop_judgment sg o MetaSimplifier.rewrite_term sg (get_atomize sg) []; |
153 drop_judgment sg o MetaSimplifier.rewrite_term sg (get_atomize sg) []; |
153 |
154 |
154 fun atomize_rule sg = Tactic.rewrite true (get_atomize sg); |
155 fun atomize_rule sg = Tactic.rewrite true (get_atomize sg); |
155 |
156 |
|
157 (*Convert a natural-deduction rule into a formula (probably in FOL)*) |
|
158 fun atomize_thm th = |
|
159 rewrite_rule (get_atomize (Thm.sign_of_thm th)) th; |
|
160 |
156 fun atomize_tac i st = |
161 fun atomize_tac i st = |
157 if Logic.has_meta_prems (Thm.prop_of st) i then |
162 if Logic.has_meta_prems (Thm.prop_of st) i then |
158 (rewrite_prems_tac (get_atomize (Thm.sign_of_thm st)) i) st |
163 (rewrite_prems_tac (get_atomize (Thm.sign_of_thm st)) i) st |
159 else all_tac st; |
164 else all_tac st; |
160 |
165 |