# HG changeset patch
# User wenzelm
# Date 1729456776 -7200
# Node ID 2fccbfca13618167e951e5fd8b4216c329491f8b
# Parent  c9235a0cde83b9a5510143e3cba9c3850b0099db
clarified concrete vs. abstract syntax;

diff -r c9235a0cde83 -r 2fccbfca1361 src/HOL/Prolog/HOHH.thy
--- a/src/HOL/Prolog/HOHH.thy	Sun Oct 20 21:51:47 2024 +0200
+++ b/src/HOL/Prolog/HOHH.thy	Sun Oct 20 22:39:36 2024 +0200
@@ -18,16 +18,16 @@
   \<open>Attrib.thms >> (fn thms => fn ctxt => SIMPLE_METHOD (Prolog.prolog_tac ctxt thms))\<close>
   "Lambda Prolog interpreter"
 
-consts
+syntax
 
 (* D-formulas (programs):  D ::= !x. D | D .. D | D :- G | A            *)
-  Dand        :: "[bool, bool] => bool"         (infixr \<open>..\<close> 28)
-  Dif        :: "[bool, bool] => bool"         (infixl \<open>:-\<close> 29)
+  "_Dand" :: "[bool, bool] => bool"         (infixr \<open>..\<close> 28)
+  "_Dif" :: "[bool, bool] => bool"         (infixl \<open>:-\<close> 29)
 
 (* G-formulas (goals):     G ::= A | G & G | G | G | ? x. G
                                | True | !x. G | D => G                  *)
-(*Dand'         :: "[bool, bool] => bool"         (infixr "," 35)*)
-  Dimp          :: "[bool, bool] => bool"         (infixr \<open>=>\<close> 27)
+(*"_Dand'" :: "[bool, bool] => bool"         (infixr "," 35)*)
+  "_Dimp" :: "[bool, bool] => bool"         (infixr \<open>=>\<close> 27)
 
 translations