src/Sequents/S43.thy
changeset 69605 3dda49e08b9d
parent 61386 0a29a984a91b
equal deleted inserted replaced
69604:a80d8ec6c998 69605:3dda49e08b9d
    18 
    18 
    19 parse_translation \<open>
    19 parse_translation \<open>
    20   let
    20   let
    21     val tr  = seq_tr;
    21     val tr  = seq_tr;
    22     fun s43pi_tr [s1, s2, s3, s4, s5, s6] =
    22     fun s43pi_tr [s1, s2, s3, s4, s5, s6] =
    23       Const (@{const_syntax S43pi}, dummyT) $ tr s1 $ tr s2 $ tr s3 $ tr s4 $ tr s5 $ tr s6;
    23       Const (\<^const_syntax>\<open>S43pi\<close>, dummyT) $ tr s1 $ tr s2 $ tr s3 $ tr s4 $ tr s5 $ tr s6;
    24   in [(@{syntax_const "_S43pi"}, K s43pi_tr)] end
    24   in [(\<^syntax_const>\<open>_S43pi\<close>, K s43pi_tr)] end
    25 \<close>
    25 \<close>
    26 
    26 
    27 print_translation \<open>
    27 print_translation \<open>
    28 let
    28 let
    29   val tr' = seq_tr';
    29   val tr' = seq_tr';
    30   fun s43pi_tr' [s1, s2, s3, s4, s5, s6] =
    30   fun s43pi_tr' [s1, s2, s3, s4, s5, s6] =
    31     Const(@{syntax_const "_S43pi"}, dummyT) $ tr' s1 $ tr' s2 $ tr' s3 $ tr' s4 $ tr' s5 $ tr' s6;
    31     Const(\<^syntax_const>\<open>_S43pi\<close>, dummyT) $ tr' s1 $ tr' s2 $ tr' s3 $ tr' s4 $ tr' s5 $ tr' s6;
    32 in [(@{const_syntax S43pi}, K s43pi_tr')] end
    32 in [(\<^const_syntax>\<open>S43pi\<close>, K s43pi_tr')] end
    33 \<close>
    33 \<close>
    34 
    34 
    35 axiomatization where
    35 axiomatization where
    36 (* Definition of the star operation using a set of Horn clauses  *)
    36 (* Definition of the star operation using a set of Horn clauses  *)
    37 (* For system S43: gamma * == {[]P | []P : gamma}                *)
    37 (* For system S43: gamma * == {[]P | []P : gamma}                *)