Mercurial Mercurial > wneuper > isa / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
src/Tools/isac/Knowledge/PolyEq.thy
changeset 60337 cbad4e18e91b
parent 60335 7701598a2182
child 60342 e96abd81a321 
     1.1 --- a/src/Tools/isac/Knowledge/PolyEq.thy	Mon Jul 19 17:29:35 2021 +0200
     1.2 +++ b/src/Tools/isac/Knowledge/PolyEq.thy	Mon Jul 19 18:29:46 2021 +0200
     1.3 @@ -337,12 +337,12 @@
     1.4  	      Rule.Eval ("HOL.eq", Prog_Expr.eval_equal "#equal_"),
     1.5                Rule.Eval ("RootEq.is_rootTerm_in", eval_is_rootTerm_in ""),
     1.6  	      Rule.Eval ("RatEq.is_ratequation_in", eval_is_ratequation_in ""),
     1.7 -	      Rule.Thm ("not_true",ThmC.numerals_to_Free @{thm not_true}),
     1.8 -	      Rule.Thm ("not_false",ThmC.numerals_to_Free @{thm not_false}),
     1.9 -	      Rule.Thm ("and_true",ThmC.numerals_to_Free @{thm and_true}),
    1.10 -	      Rule.Thm ("and_false",ThmC.numerals_to_Free @{thm and_false}),
    1.11 -	      Rule.Thm ("or_true",ThmC.numerals_to_Free @{thm or_true}),
    1.12 -	      Rule.Thm ("or_false",ThmC.numerals_to_Free @{thm or_false})
    1.13 +	      Rule.Thm ("not_true", @{thm not_true}),
    1.14 +	      Rule.Thm ("not_false", @{thm not_false}),
    1.15 +	      Rule.Thm ("and_true", @{thm and_true}),
    1.16 +	      Rule.Thm ("and_false", @{thm and_false}),
    1.17 +	      Rule.Thm ("or_true", @{thm or_true}),
    1.18 +	      Rule.Thm ("or_false", @{thm or_false})
    1.19  	       ];
    1.20  
    1.21  val PolyEq_erls =
wneuper/isa