Removed needless quotation marks
authorpaulson
Fri Dec 13 11:00:44 1996 +0100 (1996-12-13)
changeset 2378fc103154ad8f
parent 2377 ad9d2dedaeaa
child 2379 2e55b396e24c
Removed needless quotation marks
src/HOL/Auth/NS_Shared.thy
src/HOL/Auth/OtwayRees.thy
src/HOL/Auth/OtwayRees_AN.thy
src/HOL/Auth/Yahalom.thy
src/HOL/Auth/Yahalom2.thy
     1.1 --- a/src/HOL/Auth/NS_Shared.thy	Fri Dec 13 10:57:50 1996 +0100
     1.2 +++ b/src/HOL/Auth/NS_Shared.thy	Fri Dec 13 11:00:44 1996 +0100
     1.3 @@ -12,7 +12,7 @@
     1.4  
     1.5  NS_Shared = Shared + 
     1.6  
     1.7 -consts  ns_shared   :: "agent set => event list set"
     1.8 +consts  ns_shared   :: agent set => event list set
     1.9  inductive "ns_shared lost"
    1.10    intrs 
    1.11           (*Initial trace is empty*)
     2.1 --- a/src/HOL/Auth/OtwayRees.thy	Fri Dec 13 10:57:50 1996 +0100
     2.2 +++ b/src/HOL/Auth/OtwayRees.thy	Fri Dec 13 11:00:44 1996 +0100
     2.3 @@ -14,7 +14,7 @@
     2.4  
     2.5  OtwayRees = Shared + 
     2.6  
     2.7 -consts  otway   :: "agent set => event list set"
     2.8 +consts  otway   :: agent set => event list set
     2.9  inductive "otway lost"
    2.10    intrs 
    2.11           (*Initial trace is empty*)
     3.1 --- a/src/HOL/Auth/OtwayRees_AN.thy	Fri Dec 13 10:57:50 1996 +0100
     3.2 +++ b/src/HOL/Auth/OtwayRees_AN.thy	Fri Dec 13 11:00:44 1996 +0100
     3.3 @@ -14,7 +14,7 @@
     3.4  
     3.5  OtwayRees_AN = Shared + 
     3.6  
     3.7 -consts  otway   :: "agent set => event list set"
     3.8 +consts  otway   :: agent set => event list set
     3.9  inductive "otway lost"
    3.10    intrs 
    3.11           (*Initial trace is empty*)
     4.1 --- a/src/HOL/Auth/Yahalom.thy	Fri Dec 13 10:57:50 1996 +0100
     4.2 +++ b/src/HOL/Auth/Yahalom.thy	Fri Dec 13 11:00:44 1996 +0100
     4.3 @@ -12,7 +12,7 @@
     4.4  
     4.5  Yahalom = Shared + 
     4.6  
     4.7 -consts  yahalom   :: "agent set => event list set"
     4.8 +consts  yahalom   :: agent set => event list set
     4.9  inductive "yahalom lost"
    4.10    intrs 
    4.11           (*Initial trace is empty*)
     5.1 --- a/src/HOL/Auth/Yahalom2.thy	Fri Dec 13 10:57:50 1996 +0100
     5.2 +++ b/src/HOL/Auth/Yahalom2.thy	Fri Dec 13 11:00:44 1996 +0100
     5.3 @@ -16,7 +16,7 @@
     5.4  
     5.5  Yahalom2 = Shared + 
     5.6  
     5.7 -consts  yahalom   :: "agent set => event list set"
     5.8 +consts  yahalom   :: agent set => event list set
     5.9  inductive "yahalom lost"
    5.10    intrs 
    5.11           (*Initial trace is empty*)