equal
deleted
inserted
replaced
11 structure Quotient_Tacs: QUOTIENT_TACS = |
11 structure Quotient_Tacs: QUOTIENT_TACS = |
12 struct |
12 struct |
13 |
13 |
14 open Quotient_Info; |
14 open Quotient_Info; |
15 open Quotient_Term; |
15 open Quotient_Term; |
16 |
|
17 |
16 |
18 (* Since HOL_basic_ss is too "big" for us, we *) |
17 (* Since HOL_basic_ss is too "big" for us, we *) |
19 (* need to set up our own minimal simpset. *) |
18 (* need to set up our own minimal simpset. *) |
20 fun mk_minimal_ss ctxt = |
19 fun mk_minimal_ss ctxt = |
21 Simplifier.context ctxt empty_ss |
20 Simplifier.context ctxt empty_ss |
586 let |
585 let |
587 val thy = ProofContext.theory_of ctxt |
586 val thy = ProofContext.theory_of ctxt |
588 val rtrm' = HOLogic.dest_Trueprop rtrm |
587 val rtrm' = HOLogic.dest_Trueprop rtrm |
589 val qtrm' = HOLogic.dest_Trueprop qtrm |
588 val qtrm' = HOLogic.dest_Trueprop qtrm |
590 val reg_goal = |
589 val reg_goal = |
591 Syntax.check_term ctxt (regularize_trm ctxt rtrm' qtrm') |
590 Syntax.check_term ctxt (regularize_trm ctxt (rtrm', qtrm')) |
592 handle (LIFT_MATCH str) => lift_match_error ctxt str rtrm qtrm |
591 handle (LIFT_MATCH str) => lift_match_error ctxt str rtrm qtrm |
593 val inj_goal = |
592 val inj_goal = |
594 Syntax.check_term ctxt (inj_repabs_trm ctxt (reg_goal, qtrm')) |
593 Syntax.check_term ctxt (inj_repabs_trm ctxt (reg_goal, qtrm')) |
595 handle (LIFT_MATCH str) => lift_match_error ctxt str rtrm qtrm |
594 handle (LIFT_MATCH str) => lift_match_error ctxt str rtrm qtrm |
596 in |
595 in |