Mercurial Mercurial > repos > isabelle / file revision
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/MicroJava/J/Prog.thy
author wenzelm
Mon, 29 Nov 1999 15:52:49 +0100
changeset 8039 a901bafe4578
parent 8011 d14c4e9e9c8e
permissions -rw-r--r--
Goal: tuned pris;

(*  Title:      HOL/MicroJava/J/Prog.thy
    ID:         $Id$
    Author:     David von Oheimb
    Copyright   1999 Technische Universitaet Muenchen

Java program = list of class declarations
*)

Prog = Decl +

types 'c prog = "'c cdecl list"

consts

  class		:: "'c prog \\<Rightarrow> (cname \\<leadsto> 'c class)"

  is_class	:: "'c prog \\<Rightarrow> cname \\<Rightarrow> bool"
  is_type	:: "'c prog \\<Rightarrow> ty    \\<Rightarrow> bool"

defs

  class_def	"class        \\<equiv> map_of"

  is_class_def	"is_class G C \\<equiv> class G C \\<noteq> None"

primrec
"is_type G (PrimT pt) = True"
"is_type G (RefT t) = (case t of NullT \\<Rightarrow> True | ClassT C \\<Rightarrow> is_class G C)"

end
isabelle