--- a/src/HOL/Induct/QuoNestedDataType.thy Sat Oct 17 01:05:59 2009 +0200
+++ b/src/HOL/Induct/QuoNestedDataType.thy Sat Oct 17 14:43:18 2009 +0200
@@ -1,8 +1,6 @@
(* Title: HOL/Induct/QuoNestedDataType
- ID: $Id$
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 2004 University of Cambridge
-
*)
header{*Quotienting a Free Algebra Involving Nested Recursion*}
@@ -14,8 +12,8 @@
text{*Messages with encryption and decryption as free constructors.*}
datatype
freeExp = VAR nat
- | PLUS freeExp freeExp
- | FNCALL nat "freeExp list"
+ | PLUS freeExp freeExp
+ | FNCALL nat "freeExp list"
text{*The equivalence relation, which makes PLUS associative.*}