equal
deleted
inserted
replaced
10 begin |
10 begin |
11 |
11 |
12 type_synonym locvars_type = "ty err list" |
12 type_synonym locvars_type = "ty err list" |
13 type_synonym opstack_type = "ty list" |
13 type_synonym opstack_type = "ty list" |
14 type_synonym state_type = "opstack_type \<times> locvars_type" |
14 type_synonym state_type = "opstack_type \<times> locvars_type" |
15 type_synonym state = "state_type option err" -- "for Kildall" |
15 type_synonym state = "state_type option err" \<comment> "for Kildall" |
16 type_synonym method_type = "state_type option list" -- "for BVSpec" |
16 type_synonym method_type = "state_type option list" \<comment> "for BVSpec" |
17 type_synonym class_type = "sig \<Rightarrow> method_type" |
17 type_synonym class_type = "sig \<Rightarrow> method_type" |
18 type_synonym prog_type = "cname \<Rightarrow> class_type" |
18 type_synonym prog_type = "cname \<Rightarrow> class_type" |
19 |
19 |
20 |
20 |
21 definition stk_esl :: "'c prog \<Rightarrow> nat \<Rightarrow> ty list esl" where |
21 definition stk_esl :: "'c prog \<Rightarrow> nat \<Rightarrow> ty list esl" where |