Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Now starts with set_current_thy
authorpaulson
Mon, 19 Aug 1996 11:19:16 +0200
changeset 1912 947a34e00d1e
parent 1911 c27e624b6d87
child 1913 2809adb15eb0
Now starts with set_current_thy
src/HOL/ex/cla.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/ex/cla.ML	Mon Aug 19 11:18:36 1996 +0200
+++ b/src/HOL/ex/cla.ML	Mon Aug 19 11:19:16 1996 +0200
@@ -10,6 +10,8 @@
 
 writeln"File HOL/ex/cla.";
 
+set_current_thy "HOL";  (*Boosts efficiency by omitting redundant rules*)
+
 goal HOL.thy "(P --> Q | R) --> (P-->Q) | (P-->R)";
 by (Fast_tac 1);
 result();
isabelle