removed quotes from consts and syntax sections
authorclasohm
Wed Nov 29 17:01:41 1995 +0100 (1995-11-29)
changeset 13745e407f2a3323
parent 1373 f061d2435d63
child 1375 d04af07266e8
removed quotes from consts and syntax sections
src/HOL/Hoare/Arith2.thy
src/HOL/Hoare/Examples.thy
src/HOL/Hoare/Hoare.thy
src/HOL/IMP/Com.thy
src/HOL/IMP/Denotation.thy
src/HOL/IMP/Hoare.thy
src/HOL/Integ/Integ.thy
src/HOL/Lex/Auto.thy
src/HOL/Lex/AutoChopper.thy
src/HOL/Lex/Chopper.thy
src/HOL/Subst/UTerm.thy
src/HOL/Subst/Unifier.thy
     1.1 --- a/src/HOL/Hoare/Arith2.thy	Wed Nov 29 16:58:30 1995 +0100
     1.2 +++ b/src/HOL/Hoare/Arith2.thy	Wed Nov 29 17:01:41 1995 +0100
     1.3 @@ -9,12 +9,12 @@
     1.4  Arith2 = Arith +
     1.5  
     1.6  consts
     1.7 -  divides :: "[nat, nat] => bool"			(infixl 70)
     1.8 -  cd	  :: "[nat, nat, nat] => bool"
     1.9 -  gcd	  :: "[nat, nat] => nat"
    1.10 +  divides :: [nat, nat] => bool			(infixl 70)
    1.11 +  cd	  :: [nat, nat, nat] => bool
    1.12 +  gcd	  :: [nat, nat] => nat
    1.13  
    1.14 -  pow	  :: "[nat, nat] => nat"			(infixl 75)
    1.15 -  fac	  :: "nat => nat"
    1.16 +  pow	  :: [nat, nat] => nat			(infixl 75)
    1.17 +  fac	  :: nat => nat
    1.18  
    1.19  defs
    1.20    divides_def	"x divides n == 0<n & 0<x & (n mod x) = 0"
     2.1 --- a/src/HOL/Hoare/Examples.thy	Wed Nov 29 16:58:30 1995 +0100
     2.2 +++ b/src/HOL/Hoare/Examples.thy	Wed Nov 29 17:01:41 1995 +0100
     2.3 @@ -9,8 +9,8 @@
     2.4  Examples = Hoare + Arith2 +
     2.5  
     2.6  syntax
     2.7 -  "@1"	:: "nat"	("1")
     2.8 -  "@2"	:: "nat"	("2")
     2.9 +  "@1"	:: nat	("1")
    2.10 +  "@2"	:: nat	("2")
    2.11  
    2.12  translations
    2.13    "1" == "Suc(0)"
     3.1 --- a/src/HOL/Hoare/Hoare.thy	Wed Nov 29 16:58:30 1995 +0100
     3.2 +++ b/src/HOL/Hoare/Hoare.thy	Wed Nov 29 17:01:41 1995 +0100
     3.3 @@ -17,27 +17,27 @@
     3.4    'a com = "'a state => 'a state => bool" (* denotation of programs *)
     3.5  
     3.6  syntax
     3.7 -  "@Skip"       :: "'a prog"				("SKIP")
     3.8 -  "@Assign"	:: "[id, 'a] => 'a prog"		("_ := _")
     3.9 -  "@Seq"	:: "['a prog, 'a prog] => 'a prog"	("_;//_" [0,1000] 999)
    3.10 -  "@If"		:: "[bool, 'a prog, 'a prog] => 'a prog"
    3.11 +  "@Skip"       :: 'a prog				("SKIP")
    3.12 +  "@Assign"	:: [id, 'a] => 'a prog		("_ := _")
    3.13 +  "@Seq"	:: ['a prog, 'a prog] => 'a prog	("_;//_" [0,1000] 999)
    3.14 +  "@If"		:: [bool, 'a prog, 'a prog] => 'a prog
    3.15                     ("IF _//THEN//  (_)//ELSE//  (_)//END")
    3.16 -  "@While"	:: "[bool, bool, 'a prog] => 'a prog"
    3.17 +  "@While"	:: [bool, bool, 'a prog] => 'a prog
    3.18                     ("WHILE _//DO {_}//  (_)//END")
    3.19  
    3.20 -  "@Spec"	:: "[bool, 'a prog, bool] => bool"	("{_}//_//{_}")
    3.21 +  "@Spec"	:: [bool, 'a prog, bool] => bool	("{_}//_//{_}")
    3.22  
    3.23  consts
    3.24    (* semantics *)
    3.25  
    3.26 -  Skip		:: "'a com"
    3.27 -  Assign	:: "[pvar, 'a exp] => 'a com"
    3.28 -  Seq		:: "['a com, 'a com] => 'a com"
    3.29 -  Cond		:: "['a bexp, 'a com, 'a com] => 'a com"
    3.30 -  While		:: "['a bexp, 'a bexp, 'a com] => 'a com"
    3.31 -  Iter		:: "[nat, 'a bexp, 'a com] => 'a com"
    3.32 +  Skip		:: 'a com
    3.33 +  Assign	:: [pvar, 'a exp] => 'a com
    3.34 +  Seq		:: ['a com, 'a com] => 'a com
    3.35 +  Cond		:: ['a bexp, 'a com, 'a com] => 'a com
    3.36 +  While		:: ['a bexp, 'a bexp, 'a com] => 'a com
    3.37 +  Iter		:: [nat, 'a bexp, 'a com] => 'a com
    3.38  
    3.39 -  Spec		:: "['a bexp, 'a com, 'a bexp] => bool"
    3.40 +  Spec		:: ['a bexp, 'a com, 'a bexp] => bool
    3.41  
    3.42  defs
    3.43    (* denotational semantics *)
     4.1 --- a/src/HOL/IMP/Com.thy	Wed Nov 29 16:58:30 1995 +0100
     4.2 +++ b/src/HOL/IMP/Com.thy	Wed Nov 29 17:01:41 1995 +0100
     4.3 @@ -26,7 +26,7 @@
     4.4  
     4.5  (** Evaluation of arithmetic expressions **)
     4.6  consts  evala    :: "(aexp*state*nat)set"
     4.7 -       "@evala"  :: "[aexp,state,nat] => bool" ("<_,_>/ -a-> _"  [0,0,50] 50)
     4.8 +       "@evala"  :: [aexp,state,nat] => bool ("<_,_>/ -a-> _"  [0,0,50] 50)
     4.9  translations
    4.10      "<ae,sig> -a-> n" == "(ae,sig,n) : evala"
    4.11  inductive "evala"
    4.12 @@ -51,7 +51,7 @@
    4.13  
    4.14  (** Evaluation of boolean expressions **)
    4.15  consts evalb	:: "(bexp*state*bool)set"	
    4.16 -       "@evalb" :: "[bexp,state,bool] => bool" ("<_,_>/ -b-> _"  [0,0,50] 50)
    4.17 +       "@evalb" :: [bexp,state,bool] => bool ("<_,_>/ -b-> _"  [0,0,50] 50)
    4.18  
    4.19  translations
    4.20      "<be,sig> -b-> b" == "(be,sig,b) : evalb"
    4.21 @@ -79,8 +79,8 @@
    4.22  
    4.23  (** Execution of commands **)
    4.24  consts  evalc    :: "(com*state*state)set"
    4.25 -        "@evalc" :: "[com,state,state] => bool" ("<_,_>/ -c-> _" [0,0,50] 50)
    4.26 -	"assign" :: "[state,nat,loc] => state"  ("_[_'/_]"       [95,0,0] 95)
    4.27 +        "@evalc" :: [com,state,state] => bool ("<_,_>/ -c-> _" [0,0,50] 50)
    4.28 +	"assign" :: [state,nat,loc] => state  ("_[_'/_]"       [95,0,0] 95)
    4.29  
    4.30  translations
    4.31         "<ce,sig> -c-> s" == "(ce,sig,s) : evalc"
     5.1 --- a/src/HOL/IMP/Denotation.thy	Wed Nov 29 16:58:30 1995 +0100
     5.2 +++ b/src/HOL/IMP/Denotation.thy	Wed Nov 29 17:01:41 1995 +0100
     5.3 @@ -10,10 +10,10 @@
     5.4  
     5.5  types com_den = "(state*state)set"
     5.6  consts
     5.7 -  A     :: "aexp => state => nat"
     5.8 -  B     :: "bexp => state => bool"
     5.9 -  C     :: "com => com_den"
    5.10 -  Gamma :: "[bexp,com_den] => (com_den => com_den)"
    5.11 +  A     :: aexp => state => nat
    5.12 +  B     :: bexp => state => bool
    5.13 +  C     :: com => com_den
    5.14 +  Gamma :: [bexp,com_den] => (com_den => com_den)
    5.15  
    5.16  primrec A aexp
    5.17    A_nat	"A(N(n)) = (%s. n)"
     6.1 --- a/src/HOL/IMP/Hoare.thy	Wed Nov 29 16:58:30 1995 +0100
     6.2 +++ b/src/HOL/IMP/Hoare.thy	Wed Nov 29 17:01:41 1995 +0100
     6.3 @@ -8,8 +8,8 @@
     6.4  
     6.5  Hoare = Denotation +
     6.6  consts
     6.7 -  spec :: "[state=>bool,com,state=>bool] => bool"
     6.8 -(* syntax "@spec" :: "[bool,com,bool] => bool" *)
     6.9 +  spec :: [state=>bool,com,state=>bool] => bool
    6.10 +(* syntax "@spec" :: [bool,com,bool] => bool *)
    6.11            ("{{(1_)}}/ (_)/ {{(1_)}}" 10)
    6.12  defs
    6.13    spec_def "spec P c Q == !s t. (s,t) : C(c) --> P s --> Q t"
     7.1 --- a/src/HOL/Integ/Integ.thy	Wed Nov 29 16:58:30 1995 +0100
     7.2 +++ b/src/HOL/Integ/Integ.thy	Wed Nov 29 17:01:41 1995 +0100
     7.3 @@ -23,13 +23,13 @@
     7.4    int :: {ord, plus, times, minus}
     7.5  
     7.6  consts
     7.7 -  zNat        :: "nat set"
     7.8 -  znat	      :: "nat => int"	   ("$# _" [80] 80)
     7.9 -  zminus      :: "int => int"	   ("$~ _" [80] 80)
    7.10 -  znegative   :: "int => bool"
    7.11 -  zmagnitude  :: "int => int"
    7.12 -  zdiv,zmod   :: "[int,int]=>int"  (infixl 70)
    7.13 -  zpred,zsuc  :: "int=>int"
    7.14 +  zNat        :: nat set
    7.15 +  znat	      :: nat => int	   ("$# _" [80] 80)
    7.16 +  zminus      :: int => int	   ("$~ _" [80] 80)
    7.17 +  znegative   :: int => bool
    7.18 +  zmagnitude  :: int => int
    7.19 +  zdiv,zmod   :: [int,int]=>int  (infixl 70)
    7.20 +  zpred,zsuc  :: int=>int
    7.21  
    7.22  defs
    7.23    zNat_def    "zNat == {x::nat. True}"
     8.1 --- a/src/HOL/Lex/Auto.thy	Wed Nov 29 16:58:30 1995 +0100
     8.2 +++ b/src/HOL/Lex/Auto.thy	Wed Nov 29 17:01:41 1995 +0100
     8.3 @@ -17,12 +17,12 @@
     8.4  types ('a,'b)auto = "'b * ('b => 'a => 'b) * ('b => bool)"
     8.5  
     8.6  consts
     8.7 -  start :: "('a, 'b)auto => 'b"
     8.8 -  next  :: "('a, 'b)auto => ('b => 'a => 'b)"
     8.9 -  fin   :: "('a, 'b)auto => ('b => bool)"
    8.10 -  nexts :: "('a, 'b)auto => 'b => 'a list => 'b"
    8.11 -  accepts :: "('a,'b) auto => 'a list => bool"  
    8.12 -  acc_prefix :: "('a, 'b)auto => 'b => 'a list => bool"
    8.13 +  start :: ('a, 'b)auto => 'b
    8.14 +  next  :: ('a, 'b)auto => ('b => 'a => 'b)
    8.15 +  fin   :: ('a, 'b)auto => ('b => bool)
    8.16 +  nexts :: ('a, 'b)auto => 'b => 'a list => 'b
    8.17 +  accepts :: ('a,'b) auto => 'a list => bool  
    8.18 +  acc_prefix :: ('a, 'b)auto => 'b => 'a list => bool
    8.19  
    8.20  defs
    8.21    start_def "start(A) == fst(A)"
     9.1 --- a/src/HOL/Lex/AutoChopper.thy	Wed Nov 29 16:58:30 1995 +0100
     9.2 +++ b/src/HOL/Lex/AutoChopper.thy	Wed Nov 29 17:01:41 1995 +0100
     9.3 @@ -17,8 +17,8 @@
     9.4  AutoChopper = Auto + Chopper +
     9.5  
     9.6  consts
     9.7 -  is_auto_chopper :: "(('a,'b)auto => 'a chopper) => bool"
     9.8 -  auto_chopper :: "('a,'b)auto => 'a chopper"
     9.9 +  is_auto_chopper :: (('a,'b)auto => 'a chopper) => bool
    9.10 +  auto_chopper :: ('a,'b)auto => 'a chopper
    9.11    acc :: "['a list, 'b, 'a list, 'a list, 'a list list*'a list, ('a,'b)auto]
    9.12  	  => 'a list list * 'a list"
    9.13  
    10.1 --- a/src/HOL/Lex/Chopper.thy	Wed Nov 29 16:58:30 1995 +0100
    10.2 +++ b/src/HOL/Lex/Chopper.thy	Wed Nov 29 17:01:41 1995 +0100
    10.3 @@ -20,7 +20,7 @@
    10.4  types   'a chopper = "'a list => 'a list list * 'a list"
    10.5  
    10.6  consts
    10.7 -  is_longest_prefix_chopper :: "['a list => bool, 'a chopper] => bool"
    10.8 +  is_longest_prefix_chopper :: ['a list => bool, 'a chopper] => bool
    10.9  
   10.10  defs
   10.11    is_longest_prefix_chopper_def
    11.1 --- a/src/HOL/Subst/UTerm.thy	Wed Nov 29 16:58:30 1995 +0100
    11.2 +++ b/src/HOL/Subst/UTerm.thy	Wed Nov 29 17:01:41 1995 +0100
    11.3 @@ -14,15 +14,15 @@
    11.4    uterm     :: (term)term
    11.5  
    11.6  consts
    11.7 -  uterm     :: "'a item set => 'a item set"
    11.8 -  Rep_uterm :: "'a uterm => 'a item"
    11.9 -  Abs_uterm :: "'a item => 'a uterm"
   11.10 -  VAR       :: "'a item => 'a item"
   11.11 -  CONST     :: "'a item => 'a item"
   11.12 -  COMB      :: "['a item, 'a item] => 'a item"
   11.13 -  Var       :: "'a => 'a uterm"
   11.14 -  Const     :: "'a => 'a uterm"
   11.15 -  Comb      :: "['a uterm, 'a uterm] => 'a uterm"
   11.16 +  uterm     :: 'a item set => 'a item set
   11.17 +  Rep_uterm :: 'a uterm => 'a item
   11.18 +  Abs_uterm :: 'a item => 'a uterm
   11.19 +  VAR       :: 'a item => 'a item
   11.20 +  CONST     :: 'a item => 'a item
   11.21 +  COMB      :: ['a item, 'a item] => 'a item
   11.22 +  Var       :: 'a => 'a uterm
   11.23 +  Const     :: 'a => 'a uterm
   11.24 +  Comb      :: ['a uterm, 'a uterm] => 'a uterm
   11.25    UTerm_rec :: "['a item, 'a item => 'b, 'a item => 'b, 
   11.26                  ['a item , 'a item, 'b, 'b]=>'b] => 'b"
   11.27    uterm_rec :: "['a uterm, 'a => 'b, 'a => 'b, 
    12.1 --- a/src/HOL/Subst/Unifier.thy	Wed Nov 29 16:58:30 1995 +0100
    12.2 +++ b/src/HOL/Subst/Unifier.thy	Wed Nov 29 17:01:41 1995 +0100
    12.3 @@ -14,7 +14,7 @@
    12.4    ">>"       :: "[('a*('a uterm))list,('a*('a uterm))list] => bool" (infixr 52)
    12.5    MGUnifier  :: "[('a*('a uterm))list,'a uterm,'a uterm] => bool"
    12.6    MGIUnifier :: "[('a*('a uterm))list,'a uterm,'a uterm] => bool"
    12.7 -  UWFD       :: "['a uterm,'a uterm,'a uterm,'a uterm] => bool"
    12.8 +  UWFD       :: ['a uterm,'a uterm,'a uterm,'a uterm] => bool
    12.9  
   12.10  rules  (*Definitions*)
   12.11