--- a/src/HOL/Induct/QuoDataType.thy Sat Oct 17 01:05:59 2009 +0200
+++ b/src/HOL/Induct/QuoDataType.thy Sat Oct 17 14:43:18 2009 +0200
@@ -1,8 +1,6 @@
(* Title: HOL/Induct/QuoDataType
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 2004 University of Cambridge
-
*)
header{*Defining an Initial Algebra by Quotienting a Free Algebra*}
@@ -14,9 +12,9 @@
text{*Messages with encryption and decryption as free constructors.*}
datatype
freemsg = NONCE nat
- | MPAIR freemsg freemsg
- | CRYPT nat freemsg
- | DECRYPT nat freemsg
+ | MPAIR freemsg freemsg
+ | CRYPT nat freemsg
+ | DECRYPT nat freemsg
text{*The equivalence relation, which makes encryption and decryption inverses
provided the keys are the same.