equal
deleted
inserted
replaced
7 theory JVMListExample |
7 theory JVMListExample |
8 imports "../J/SystemClasses" JVMExec |
8 imports "../J/SystemClasses" JVMExec |
9 begin |
9 begin |
10 |
10 |
11 text \<open> |
11 text \<open> |
12 Since the types @{typ cnam}, \<open>vnam\<close>, and \<open>mname\<close> are |
12 Since the types \<^typ>\<open>cnam\<close>, \<open>vnam\<close>, and \<open>mname\<close> are |
13 anonymous, we describe distinctness of names in the example by axioms: |
13 anonymous, we describe distinctness of names in the example by axioms: |
14 \<close> |
14 \<close> |
15 axiomatization list_nam test_nam :: cnam |
15 axiomatization list_nam test_nam :: cnam |
16 where distinct_classes: "list_nam \<noteq> test_nam" |
16 where distinct_classes: "list_nam \<noteq> test_nam" |
17 |
17 |