| changeset 30552 | 58db56278478 |
| parent 30528 | 7173bf123335 |
| child 30722 | 623d4831c8cf |
| 30551:24e156db414c | 30552:58db56278478 |
|---|---|
300 |
300 |
301 val rulify = |
301 val rulify = |
302 hol_simplify inductive_conj |
302 hol_simplify inductive_conj |
303 #> hol_simplify inductive_rulify |
303 #> hol_simplify inductive_rulify |
304 #> hol_simplify inductive_rulify_fallback |
304 #> hol_simplify inductive_rulify_fallback |
305 #> MetaSimplifier.norm_hhf; |
305 #> Simplifier.norm_hhf; |
306 |
306 |
307 end; |
307 end; |
308 |
308 |
309 |
309 |
310 |
310 |