Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
clarified concrete vs. abstract syntax;
authorwenzelm
Sun, 20 Oct 2024 22:39:36 +0200
changeset 81216 2fccbfca1361
parent 81215 c9235a0cde83
child 81217 6a33337eb08d
clarified concrete vs. abstract syntax;
src/HOL/Prolog/HOHH.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle