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/MicroJava/Comp/Index.thy
changeset 46742 125e49d04cf6
parent 46226 e88e980ed735
child 55417 01fbfb60c33e 
--- a/src/HOL/MicroJava/Comp/Index.thy	Thu Mar 01 14:42:05 2012 +0100
+++ b/src/HOL/MicroJava/Comp/Index.thy	Thu Mar 01 14:48:28 2012 +0100
@@ -127,7 +127,7 @@
 lemma wf_java_mdecl_disjoint_varnames: 
   "wf_java_mdecl G C (S,rT,(pns,lvars,blk,res)) 
   \<Longrightarrow> disjoint_varnames pns lvars"
-apply (case_tac S)
+apply (cases S)
 apply (simp add: wf_java_mdecl_def disjoint_varnames_def  map_of_in_set)
 done
isabelle