# HG changeset patch # User paulson # Date 850471244 -3600 # Node ID fc103154ad8fce3876d2b287892d62416322d7c3 # Parent ad9d2dedaeaa8d6f17ee22573cf3df510881c359 Removed needless quotation marks diff -r ad9d2dedaeaa -r fc103154ad8f src/HOL/Auth/NS_Shared.thy --- a/src/HOL/Auth/NS_Shared.thy Fri Dec 13 10:57:50 1996 +0100 +++ b/src/HOL/Auth/NS_Shared.thy Fri Dec 13 11:00:44 1996 +0100 @@ -12,7 +12,7 @@ NS_Shared = Shared + -consts ns_shared :: "agent set => event list set" +consts ns_shared :: agent set => event list set inductive "ns_shared lost" intrs (*Initial trace is empty*) diff -r ad9d2dedaeaa -r fc103154ad8f src/HOL/Auth/OtwayRees.thy --- a/src/HOL/Auth/OtwayRees.thy Fri Dec 13 10:57:50 1996 +0100 +++ b/src/HOL/Auth/OtwayRees.thy Fri Dec 13 11:00:44 1996 +0100 @@ -14,7 +14,7 @@ OtwayRees = Shared + -consts otway :: "agent set => event list set" +consts otway :: agent set => event list set inductive "otway lost" intrs (*Initial trace is empty*) diff -r ad9d2dedaeaa -r fc103154ad8f src/HOL/Auth/OtwayRees_AN.thy --- a/src/HOL/Auth/OtwayRees_AN.thy Fri Dec 13 10:57:50 1996 +0100 +++ b/src/HOL/Auth/OtwayRees_AN.thy Fri Dec 13 11:00:44 1996 +0100 @@ -14,7 +14,7 @@ OtwayRees_AN = Shared + -consts otway :: "agent set => event list set" +consts otway :: agent set => event list set inductive "otway lost" intrs (*Initial trace is empty*) diff -r ad9d2dedaeaa -r fc103154ad8f src/HOL/Auth/Yahalom.thy --- a/src/HOL/Auth/Yahalom.thy Fri Dec 13 10:57:50 1996 +0100 +++ b/src/HOL/Auth/Yahalom.thy Fri Dec 13 11:00:44 1996 +0100 @@ -12,7 +12,7 @@ Yahalom = Shared + -consts yahalom :: "agent set => event list set" +consts yahalom :: agent set => event list set inductive "yahalom lost" intrs (*Initial trace is empty*) diff -r ad9d2dedaeaa -r fc103154ad8f src/HOL/Auth/Yahalom2.thy --- a/src/HOL/Auth/Yahalom2.thy Fri Dec 13 10:57:50 1996 +0100 +++ b/src/HOL/Auth/Yahalom2.thy Fri Dec 13 11:00:44 1996 +0100 @@ -16,7 +16,7 @@ Yahalom2 = Shared + -consts yahalom :: "agent set => event list set" +consts yahalom :: agent set => event list set inductive "yahalom lost" intrs (*Initial trace is empty*)