equal
deleted
inserted
replaced
8 theory QuoDataType imports Main begin |
8 theory QuoDataType imports Main begin |
9 |
9 |
10 subsection{*Defining the Free Algebra*} |
10 subsection{*Defining the Free Algebra*} |
11 |
11 |
12 text{*Messages with encryption and decryption as free constructors.*} |
12 text{*Messages with encryption and decryption as free constructors.*} |
13 datatype_new |
13 datatype |
14 freemsg = NONCE nat |
14 freemsg = NONCE nat |
15 | MPAIR freemsg freemsg |
15 | MPAIR freemsg freemsg |
16 | CRYPT nat freemsg |
16 | CRYPT nat freemsg |
17 | DECRYPT nat freemsg |
17 | DECRYPT nat freemsg |
18 |
18 |