equal
deleted
inserted
replaced
1080 local |
1080 local |
1081 |
1081 |
1082 val msg1 = "Regularize proof failed." |
1082 val msg1 = "Regularize proof failed." |
1083 val msg2 = cat_lines ["Injection proof failed.", |
1083 val msg2 = cat_lines ["Injection proof failed.", |
1084 "This is probably due to missing respects lemmas.", |
1084 "This is probably due to missing respects lemmas.", |
1085 "Try invoking the injection_tac manually to see", |
1085 "Try invoking the injection method manually to see", |
1086 "which lemmas are missing."] |
1086 "which lemmas are missing."] |
1087 val msg3 = "Cleaning proof failed." |
1087 val msg3 = "Cleaning proof failed." |
1088 |
1088 |
1089 in |
1089 in |
1090 |
1090 |