equal
deleted
inserted
replaced
1 (* Title: HOL/MicroJava/J/JBasis.thy |
1 (* Title: HOL/MicroJava/J/JBasis.thy |
2 Author: David von Oheimb, TU Muenchen |
2 Author: David von Oheimb, TU Muenchen |
3 *) |
3 *) |
4 |
4 |
5 chapter {* Java Source Language \label{cha:j} *} |
5 chapter \<open>Java Source Language \label{cha:j}\<close> |
6 |
6 |
7 section {* Some Auxiliary Definitions *} |
7 section \<open>Some Auxiliary Definitions\<close> |
8 |
8 |
9 theory JBasis imports Main "~~/src/HOL/Library/Transitive_Closure_Table" begin |
9 theory JBasis imports Main "~~/src/HOL/Library/Transitive_Closure_Table" begin |
10 |
10 |
11 lemmas [simp] = Let_def |
11 lemmas [simp] = Let_def |
12 |
12 |