# HG changeset patch # User clasohm # Date 817660901 -3600 # Node ID 5e407f2a332398d327da3c2aa867a3e149f91a49 # Parent f061d2435d63a74d5754acd8f7c7145b02c7492c removed quotes from consts and syntax sections diff -r f061d2435d63 -r 5e407f2a3323 src/HOL/Hoare/Arith2.thy --- a/src/HOL/Hoare/Arith2.thy Wed Nov 29 16:58:30 1995 +0100 +++ b/src/HOL/Hoare/Arith2.thy Wed Nov 29 17:01:41 1995 +0100 @@ -9,12 +9,12 @@ Arith2 = Arith + consts - divides :: "[nat, nat] => bool" (infixl 70) - cd :: "[nat, nat, nat] => bool" - gcd :: "[nat, nat] => nat" + divides :: [nat, nat] => bool (infixl 70) + cd :: [nat, nat, nat] => bool + gcd :: [nat, nat] => nat - pow :: "[nat, nat] => nat" (infixl 75) - fac :: "nat => nat" + pow :: [nat, nat] => nat (infixl 75) + fac :: nat => nat defs divides_def "x divides n == 0 'a prog" ("_ := _") - "@Seq" :: "['a prog, 'a prog] => 'a prog" ("_;//_" [0,1000] 999) - "@If" :: "[bool, 'a prog, 'a prog] => 'a prog" + "@Skip" :: 'a prog ("SKIP") + "@Assign" :: [id, 'a] => 'a prog ("_ := _") + "@Seq" :: ['a prog, 'a prog] => 'a prog ("_;//_" [0,1000] 999) + "@If" :: [bool, 'a prog, 'a prog] => 'a prog ("IF _//THEN// (_)//ELSE// (_)//END") - "@While" :: "[bool, bool, 'a prog] => 'a prog" + "@While" :: [bool, bool, 'a prog] => 'a prog ("WHILE _//DO {_}// (_)//END") - "@Spec" :: "[bool, 'a prog, bool] => bool" ("{_}//_//{_}") + "@Spec" :: [bool, 'a prog, bool] => bool ("{_}//_//{_}") consts (* semantics *) - Skip :: "'a com" - Assign :: "[pvar, 'a exp] => 'a com" - Seq :: "['a com, 'a com] => 'a com" - Cond :: "['a bexp, 'a com, 'a com] => 'a com" - While :: "['a bexp, 'a bexp, 'a com] => 'a com" - Iter :: "[nat, 'a bexp, 'a com] => 'a com" + Skip :: 'a com + Assign :: [pvar, 'a exp] => 'a com + Seq :: ['a com, 'a com] => 'a com + Cond :: ['a bexp, 'a com, 'a com] => 'a com + While :: ['a bexp, 'a bexp, 'a com] => 'a com + Iter :: [nat, 'a bexp, 'a com] => 'a com - Spec :: "['a bexp, 'a com, 'a bexp] => bool" + Spec :: ['a bexp, 'a com, 'a bexp] => bool defs (* denotational semantics *) diff -r f061d2435d63 -r 5e407f2a3323 src/HOL/IMP/Com.thy --- a/src/HOL/IMP/Com.thy Wed Nov 29 16:58:30 1995 +0100 +++ b/src/HOL/IMP/Com.thy Wed Nov 29 17:01:41 1995 +0100 @@ -26,7 +26,7 @@ (** Evaluation of arithmetic expressions **) consts evala :: "(aexp*state*nat)set" - "@evala" :: "[aexp,state,nat] => bool" ("<_,_>/ -a-> _" [0,0,50] 50) + "@evala" :: [aexp,state,nat] => bool ("<_,_>/ -a-> _" [0,0,50] 50) translations " -a-> n" == "(ae,sig,n) : evala" inductive "evala" @@ -51,7 +51,7 @@ (** Evaluation of boolean expressions **) consts evalb :: "(bexp*state*bool)set" - "@evalb" :: "[bexp,state,bool] => bool" ("<_,_>/ -b-> _" [0,0,50] 50) + "@evalb" :: [bexp,state,bool] => bool ("<_,_>/ -b-> _" [0,0,50] 50) translations " -b-> b" == "(be,sig,b) : evalb" @@ -79,8 +79,8 @@ (** Execution of commands **) consts evalc :: "(com*state*state)set" - "@evalc" :: "[com,state,state] => bool" ("<_,_>/ -c-> _" [0,0,50] 50) - "assign" :: "[state,nat,loc] => state" ("_[_'/_]" [95,0,0] 95) + "@evalc" :: [com,state,state] => bool ("<_,_>/ -c-> _" [0,0,50] 50) + "assign" :: [state,nat,loc] => state ("_[_'/_]" [95,0,0] 95) translations " -c-> s" == "(ce,sig,s) : evalc" diff -r f061d2435d63 -r 5e407f2a3323 src/HOL/IMP/Denotation.thy --- a/src/HOL/IMP/Denotation.thy Wed Nov 29 16:58:30 1995 +0100 +++ b/src/HOL/IMP/Denotation.thy Wed Nov 29 17:01:41 1995 +0100 @@ -10,10 +10,10 @@ types com_den = "(state*state)set" consts - A :: "aexp => state => nat" - B :: "bexp => state => bool" - C :: "com => com_den" - Gamma :: "[bexp,com_den] => (com_den => com_den)" + A :: aexp => state => nat + B :: bexp => state => bool + C :: com => com_den + Gamma :: [bexp,com_den] => (com_den => com_den) primrec A aexp A_nat "A(N(n)) = (%s. n)" diff -r f061d2435d63 -r 5e407f2a3323 src/HOL/IMP/Hoare.thy --- a/src/HOL/IMP/Hoare.thy Wed Nov 29 16:58:30 1995 +0100 +++ b/src/HOL/IMP/Hoare.thy Wed Nov 29 17:01:41 1995 +0100 @@ -8,8 +8,8 @@ Hoare = Denotation + consts - spec :: "[state=>bool,com,state=>bool] => bool" -(* syntax "@spec" :: "[bool,com,bool] => bool" *) + spec :: [state=>bool,com,state=>bool] => bool +(* syntax "@spec" :: [bool,com,bool] => bool *) ("{{(1_)}}/ (_)/ {{(1_)}}" 10) defs spec_def "spec P c Q == !s t. (s,t) : C(c) --> P s --> Q t" diff -r f061d2435d63 -r 5e407f2a3323 src/HOL/Integ/Integ.thy --- a/src/HOL/Integ/Integ.thy Wed Nov 29 16:58:30 1995 +0100 +++ b/src/HOL/Integ/Integ.thy Wed Nov 29 17:01:41 1995 +0100 @@ -23,13 +23,13 @@ int :: {ord, plus, times, minus} consts - zNat :: "nat set" - znat :: "nat => int" ("$# _" [80] 80) - zminus :: "int => int" ("$~ _" [80] 80) - znegative :: "int => bool" - zmagnitude :: "int => int" - zdiv,zmod :: "[int,int]=>int" (infixl 70) - zpred,zsuc :: "int=>int" + zNat :: nat set + znat :: nat => int ("$# _" [80] 80) + zminus :: int => int ("$~ _" [80] 80) + znegative :: int => bool + zmagnitude :: int => int + zdiv,zmod :: [int,int]=>int (infixl 70) + zpred,zsuc :: int=>int defs zNat_def "zNat == {x::nat. True}" diff -r f061d2435d63 -r 5e407f2a3323 src/HOL/Lex/Auto.thy --- a/src/HOL/Lex/Auto.thy Wed Nov 29 16:58:30 1995 +0100 +++ b/src/HOL/Lex/Auto.thy Wed Nov 29 17:01:41 1995 +0100 @@ -17,12 +17,12 @@ types ('a,'b)auto = "'b * ('b => 'a => 'b) * ('b => bool)" consts - start :: "('a, 'b)auto => 'b" - next :: "('a, 'b)auto => ('b => 'a => 'b)" - fin :: "('a, 'b)auto => ('b => bool)" - nexts :: "('a, 'b)auto => 'b => 'a list => 'b" - accepts :: "('a,'b) auto => 'a list => bool" - acc_prefix :: "('a, 'b)auto => 'b => 'a list => bool" + start :: ('a, 'b)auto => 'b + next :: ('a, 'b)auto => ('b => 'a => 'b) + fin :: ('a, 'b)auto => ('b => bool) + nexts :: ('a, 'b)auto => 'b => 'a list => 'b + accepts :: ('a,'b) auto => 'a list => bool + acc_prefix :: ('a, 'b)auto => 'b => 'a list => bool defs start_def "start(A) == fst(A)" diff -r f061d2435d63 -r 5e407f2a3323 src/HOL/Lex/AutoChopper.thy --- a/src/HOL/Lex/AutoChopper.thy Wed Nov 29 16:58:30 1995 +0100 +++ b/src/HOL/Lex/AutoChopper.thy Wed Nov 29 17:01:41 1995 +0100 @@ -17,8 +17,8 @@ AutoChopper = Auto + Chopper + consts - is_auto_chopper :: "(('a,'b)auto => 'a chopper) => bool" - auto_chopper :: "('a,'b)auto => 'a chopper" + is_auto_chopper :: (('a,'b)auto => 'a chopper) => bool + auto_chopper :: ('a,'b)auto => 'a chopper acc :: "['a list, 'b, 'a list, 'a list, 'a list list*'a list, ('a,'b)auto] => 'a list list * 'a list" diff -r f061d2435d63 -r 5e407f2a3323 src/HOL/Lex/Chopper.thy --- a/src/HOL/Lex/Chopper.thy Wed Nov 29 16:58:30 1995 +0100 +++ b/src/HOL/Lex/Chopper.thy Wed Nov 29 17:01:41 1995 +0100 @@ -20,7 +20,7 @@ types 'a chopper = "'a list => 'a list list * 'a list" consts - is_longest_prefix_chopper :: "['a list => bool, 'a chopper] => bool" + is_longest_prefix_chopper :: ['a list => bool, 'a chopper] => bool defs is_longest_prefix_chopper_def diff -r f061d2435d63 -r 5e407f2a3323 src/HOL/Subst/UTerm.thy --- a/src/HOL/Subst/UTerm.thy Wed Nov 29 16:58:30 1995 +0100 +++ b/src/HOL/Subst/UTerm.thy Wed Nov 29 17:01:41 1995 +0100 @@ -14,15 +14,15 @@ uterm :: (term)term consts - uterm :: "'a item set => 'a item set" - Rep_uterm :: "'a uterm => 'a item" - Abs_uterm :: "'a item => 'a uterm" - VAR :: "'a item => 'a item" - CONST :: "'a item => 'a item" - COMB :: "['a item, 'a item] => 'a item" - Var :: "'a => 'a uterm" - Const :: "'a => 'a uterm" - Comb :: "['a uterm, 'a uterm] => 'a uterm" + uterm :: 'a item set => 'a item set + Rep_uterm :: 'a uterm => 'a item + Abs_uterm :: 'a item => 'a uterm + VAR :: 'a item => 'a item + CONST :: 'a item => 'a item + COMB :: ['a item, 'a item] => 'a item + Var :: 'a => 'a uterm + Const :: 'a => 'a uterm + Comb :: ['a uterm, 'a uterm] => 'a uterm UTerm_rec :: "['a item, 'a item => 'b, 'a item => 'b, ['a item , 'a item, 'b, 'b]=>'b] => 'b" uterm_rec :: "['a uterm, 'a => 'b, 'a => 'b, diff -r f061d2435d63 -r 5e407f2a3323 src/HOL/Subst/Unifier.thy --- a/src/HOL/Subst/Unifier.thy Wed Nov 29 16:58:30 1995 +0100 +++ b/src/HOL/Subst/Unifier.thy Wed Nov 29 17:01:41 1995 +0100 @@ -14,7 +14,7 @@ ">>" :: "[('a*('a uterm))list,('a*('a uterm))list] => bool" (infixr 52) MGUnifier :: "[('a*('a uterm))list,'a uterm,'a uterm] => bool" MGIUnifier :: "[('a*('a uterm))list,'a uterm,'a uterm] => bool" - UWFD :: "['a uterm,'a uterm,'a uterm,'a uterm] => bool" + UWFD :: ['a uterm,'a uterm,'a uterm,'a uterm] => bool rules (*Definitions*)