equal
deleted
inserted
replaced
5 section \<open>From Types to Sets\<close> |
5 section \<open>From Types to Sets\<close> |
6 |
6 |
7 text \<open>This theory extends Isabelle/HOL's logic by two new inference rules |
7 text \<open>This theory extends Isabelle/HOL's logic by two new inference rules |
8 to allow translation of types to sets as described in |
8 to allow translation of types to sets as described in |
9 O. Kunčar, A. Popescu: From Types to Sets by Local Type Definitions in Higher-Order Logic |
9 O. Kunčar, A. Popescu: From Types to Sets by Local Type Definitions in Higher-Order Logic |
10 available at http://www21.in.tum.de/~kuncar/documents/kuncar-popescu-t2s2016-extended.pdf.\<close> |
10 available at https://www21.in.tum.de/~kuncar/documents/kuncar-popescu-t2s2016-extended.pdf.\<close> |
11 |
11 |
12 theory Types_To_Sets |
12 theory Types_To_Sets |
13 imports Main |
13 imports Main |
14 begin |
14 begin |
15 |
15 |