1.1 --- a/test/Tools/isac/Knowledge/polyminus.sml Mon Jul 19 17:29:35 2021 +0200
1.2 +++ b/test/Tools/isac/Knowledge/polyminus.sml Mon Jul 19 18:29:46 2021 +0200
1.3 @@ -706,9 +706,9 @@
1.4 (*"(?a | True) = True"*)
1.5 Thm ("or_false",@{thm or_false}),
1.6 (*"(?a | False) = ?a"*)
1.7 - Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
1.8 + Thm ("not_true", @{thm not_true}),
1.9 (*"(~ True) = False"*)
1.10 - Thm ("not_false",ThmC.numerals_to_Free @{thm not_false})
1.11 + Thm ("not_false", @{thm not_false})
1.12 (*"(~ False) = True"*)];
1.13 (*Rewrite.trace_on := true; ..stopped Test_Isac.thy*)
1.14 val SOME (t', _) = rewrite_set_ thy false prls t;