src/Sequents/S43.thy
changeset 14765 bafb24c150c1
parent 2073 fb0655539d05
child 17481 75166ebb619b
equal deleted inserted replaced
14764:5d8a9900cabc 14765:bafb24c150c1
     9 S43 = Modal0 +
     9 S43 = Modal0 +
    10 
    10 
    11 consts
    11 consts
    12   S43pi :: "[seq'=>seq', seq'=>seq', seq'=>seq',
    12   S43pi :: "[seq'=>seq', seq'=>seq', seq'=>seq',
    13              seq'=>seq', seq'=>seq', seq'=>seq'] => prop"
    13              seq'=>seq', seq'=>seq', seq'=>seq'] => prop"
       
    14 syntax
    14   "@S43pi" :: "[seq, seq, seq, seq, seq, seq] => prop"
    15   "@S43pi" :: "[seq, seq, seq, seq, seq, seq] => prop"
    15                          ("S43pi((_);(_);(_);(_);(_);(_))" [] 5)
    16                          ("S43pi((_);(_);(_);(_);(_);(_))" [] 5)
    16 
    17 
    17 rules
    18 rules
    18 (* Definition of the star operation using a set of Horn clauses  *)
    19 (* Definition of the star operation using a set of Horn clauses  *)