removed quotes from types section
authorclasohm
Fri Dec 01 14:17:50 1995 +0100 (1995-12-01)
changeset 1384007ad29ce6ca
parent 1383 be42217b0b5c
child 1385 63c3d78df538
removed quotes from types section
src/HOL/Hoare/Hoare.thy
src/HOL/MiniML/Type.thy
src/HOL/Univ.thy
src/HOL/ex/String.thy
     1.1 --- a/src/HOL/Hoare/Hoare.thy	Fri Dec 01 13:54:27 1995 +0100
     1.2 +++ b/src/HOL/Hoare/Hoare.thy	Fri Dec 01 14:17:50 1995 +0100
     1.3 @@ -10,11 +10,11 @@
     1.4  
     1.5  types
     1.6    'a prog			(* program syntax *)
     1.7 -  pvar = "nat"			(* encoding of program variables ( < 26! ) *)
     1.8 -  'a state = "pvar => 'a"	(* program state *)
     1.9 -  'a exp ="'a state => 'a"	(* denotation of expressions *)
    1.10 -  'a bexp = "'a state => bool"  (* denotation of boolean expressions *)
    1.11 -  'a com = "'a state => 'a state => bool" (* denotation of programs *)
    1.12 +  pvar = nat			(* encoding of program variables ( < 26! ) *)
    1.13 +  'a state = pvar => 'a		(* program state *)
    1.14 +  'a exp = 'a state => 'a	(* denotation of expressions *)
    1.15 +  'a bexp = 'a state => bool	(* denotation of boolean expressions *)
    1.16 +  'a com = 'a state => 'a state => bool (* denotation of programs *)
    1.17  
    1.18  syntax
    1.19    "@Skip"       :: 'a prog				("SKIP")
     2.1 --- a/src/HOL/MiniML/Type.thy	Fri Dec 01 13:54:27 1995 +0100
     2.2 +++ b/src/HOL/MiniML/Type.thy	Fri Dec 01 14:17:50 1995 +0100
     2.3 @@ -18,7 +18,7 @@
     2.4  
     2.5  (* type variable substitution *)
     2.6  types
     2.7 -	subst = "nat => type_expr"
     2.8 +	subst = nat => type_expr
     2.9  
    2.10  arities
    2.11  	type_expr::type_struct
     3.1 --- a/src/HOL/Univ.thy	Fri Dec 01 13:54:27 1995 +0100
     3.2 +++ b/src/HOL/Univ.thy	Fri Dec 01 14:17:50 1995 +0100
     3.3 @@ -19,7 +19,7 @@
     3.4    'a node = "{p. EX f x k. p = (f::nat=>nat, x::'a+nat) & f(k)=0}"
     3.5  
     3.6  types
     3.7 -  'a item = "'a node set"
     3.8 +  'a item = 'a node set
     3.9  
    3.10  consts
    3.11    Least     :: (nat=>bool) => nat    (binder "LEAST " 10)
     4.1 --- a/src/HOL/ex/String.thy	Fri Dec 01 13:54:27 1995 +0100
     4.2 +++ b/src/HOL/ex/String.thy	Fri Dec 01 14:17:50 1995 +0100
     4.3 @@ -14,7 +14,7 @@
     4.4    char = Char nibble nibble
     4.5  
     4.6  types
     4.7 -  string = "char list"
     4.8 +  string = char list
     4.9  
    4.10  syntax
    4.11    "_Char"       :: xstr => char       ("CHR _")