Mercurial Mercurial > repos > isabelle / diff
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/NanoJava/TypeRel.thy
changeset 35416 d8d7d1b785af
parent 35102 cc7a0b9f938c
child 41589 bbd861837ebc 
--- a/src/HOL/NanoJava/TypeRel.thy	Wed Feb 24 11:55:52 2010 +0100
+++ b/src/HOL/NanoJava/TypeRel.thy	Mon Mar 01 13:40:23 2010 +0100
@@ -66,9 +66,7 @@
 apply  auto
 done
 
-constdefs
-
-  ws_prog  :: "bool"
+definition ws_prog :: "bool" where
  "ws_prog \<equiv> \<forall>(C,c)\<in>set Prog. C\<noteq>Object \<longrightarrow> 
                               is_class (super c) \<and> (super c,C)\<notin>subcls1^+"
isabelle