changeset 54883 | dd04a8b654fc |
parent 54742 | 7a86358a3c0b |
child 55111 | 5792f5106c40 |
54882:61276a7fc369 | 54883:dd04a8b654fc |
---|---|
355 |
355 |
356 fun rulify ctxt = |
356 fun rulify ctxt = |
357 hol_simplify ctxt inductive_conj |
357 hol_simplify ctxt inductive_conj |
358 #> hol_simplify ctxt inductive_rulify |
358 #> hol_simplify ctxt inductive_rulify |
359 #> hol_simplify ctxt inductive_rulify_fallback |
359 #> hol_simplify ctxt inductive_rulify_fallback |
360 #> Simplifier.norm_hhf; |
360 #> Simplifier.norm_hhf ctxt; |
361 |
361 |
362 end; |
362 end; |
363 |
363 |
364 |
364 |
365 |
365 |