src/HOL/Hoare_Parallel/Quote_Antiquote.thy
author blanchet
Tue Nov 07 15:16:42 2017 +0100 (20 months ago)
changeset 67022 49309fe530fd
parent 62390 842917225d56
child 69597 ff784d5a5bfb
permissions -rw-r--r--
more robust parsing for THF proofs (esp. polymorphic Leo-III proofs)
     1 section \<open>Concrete Syntax\<close>
     2 
     3 theory Quote_Antiquote imports Main begin
     4 
     5 syntax
     6   "_quote"     :: "'b \<Rightarrow> ('a \<Rightarrow> 'b)"                ("(\<guillemotleft>_\<guillemotright>)" [0] 1000)
     7   "_antiquote" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'b"                ("\<acute>_" [1000] 1000)
     8   "_Assert"    :: "'a \<Rightarrow> 'a set"                    ("(\<lbrace>_\<rbrace>)" [0] 1000)
     9 
    10 translations
    11   "\<lbrace>b\<rbrace>" \<rightharpoonup> "CONST Collect \<guillemotleft>b\<guillemotright>"
    12 
    13 parse_translation \<open>
    14   let
    15     fun quote_tr [t] = Syntax_Trans.quote_tr @{syntax_const "_antiquote"} t
    16       | quote_tr ts = raise TERM ("quote_tr", ts);
    17   in [(@{syntax_const "_quote"}, K quote_tr)] end
    18 \<close>
    19 
    20 end