equal
deleted
inserted
replaced
27 |
27 |
28 (** various helper fuctions **) |
28 (** various helper fuctions **) |
29 |
29 |
30 (* Since HOL_basic_ss is too "big" for us, we *) |
30 (* Since HOL_basic_ss is too "big" for us, we *) |
31 (* need to set up our own minimal simpset. *) |
31 (* need to set up our own minimal simpset. *) |
32 fun mk_minimal_ss ctxt = |
32 fun mk_minimal_ss ctxt = |
33 Simplifier.context ctxt empty_ss |
33 Simplifier.context ctxt empty_ss |
34 setsubgoaler asm_simp_tac |
34 setsubgoaler asm_simp_tac |
35 setmksimps (mksimps []) |
35 setmksimps (mksimps []) |
36 |
36 |
37 (* composition of two theorems, used in maps *) |
37 (* composition of two theorems, used in maps *) |