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/Library/SCT_Implementation.thy
changeset 23394 474ff28210c0
parent 23374 a2f492c599e0
child 23416 b73a6b72f706 
--- a/src/HOL/Library/SCT_Implementation.thy	Thu Jun 14 23:04:36 2007 +0200
+++ b/src/HOL/Library/SCT_Implementation.thy	Thu Jun 14 23:04:39 2007 +0200
@@ -88,9 +88,9 @@
   assumes "A \<le> B"
   assumes "no_bad_graphs B"
   shows "no_bad_graphs A"
-using prems
-unfolding no_bad_graphs_def has_edge_def graph_leq_def 
-by blast
+  using assms
+  unfolding no_bad_graphs_def has_edge_def graph_leq_def 
+  by blast
isabelle