author | wenzelm |
Sun, 12 Sep 2021 20:14:09 +0200 | |
changeset 74300 | 33f13d2d211c |
parent 74299 | 16e5870fe21e |
child 74301 | ffe269e74bdd |
src/FOL/FOL.thy | file | annotate | diff | comparison | revisions |
--- a/src/FOL/FOL.thy Sun Sep 12 20:11:20 2021 +0200 +++ b/src/FOL/FOL.thy Sun Sep 12 20:14:09 2021 +0200 @@ -203,7 +203,7 @@ structure Blast = Blast ( structure Classical = Cla - val Trueprop_const = dest_Const \<^const>\<open>Trueprop\<close> + val Trueprop_const = dest_Const \<^Const>\<open>Trueprop\<close> val equality_name = \<^const_name>\<open>eq\<close> val not_name = \<^const_name>\<open>Not\<close> val notE = @{thm notE}