equal
deleted
inserted
replaced
2 imports QuotScript Prove |
2 imports QuotScript Prove |
3 uses ("quotient_info.ML") |
3 uses ("quotient_info.ML") |
4 ("quotient.ML") |
4 ("quotient.ML") |
5 ("quotient_def.ML") |
5 ("quotient_def.ML") |
6 begin |
6 begin |
7 |
|
8 |
7 |
9 locale QUOT_TYPE = |
8 locale QUOT_TYPE = |
10 fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
9 fixes R :: "'a \<Rightarrow> 'a \<Rightarrow> bool" |
11 and Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b" |
10 and Abs :: "('a \<Rightarrow> bool) \<Rightarrow> 'b" |
12 and Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)" |
11 and Rep :: "'b \<Rightarrow> ('a \<Rightarrow> bool)" |
1019 ML {* |
1018 ML {* |
1020 fun lift_match_error ctxt fun_str rtrm qtrm = |
1019 fun lift_match_error ctxt fun_str rtrm qtrm = |
1021 let |
1020 let |
1022 val rtrm_str = Syntax.string_of_term ctxt rtrm |
1021 val rtrm_str = Syntax.string_of_term ctxt rtrm |
1023 val qtrm_str = Syntax.string_of_term ctxt qtrm |
1022 val qtrm_str = Syntax.string_of_term ctxt qtrm |
1024 val msg = [enclose "[" "]" fun_str, "The quotient theorem\n", qtrm_str, |
1023 val msg = cat_lines [enclose "[" "]" fun_str, "The quotient theorem", qtrm_str, |
1025 "and the lifted theorem\n", rtrm_str, "do not match"] |
1024 "", "does not match with original theorem", rtrm_str] |
1026 in |
1025 in |
1027 error (space_implode " " msg) |
1026 error msg |
1028 end |
1027 end |
1029 *} |
1028 *} |
1030 |
1029 |
1031 ML {* |
1030 ML {* |
1032 fun procedure_inst ctxt rtrm qtrm = |
1031 fun procedure_inst ctxt rtrm qtrm = |