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.
Isar "default" step needs to fail for solved problems, for clear distinction of '.' and '..' for example -- amending lapse introduced in 9de4d64eee3b (April 2004);
authorwenzelm
Thu, 16 Sep 2010 15:37:12 +0200
changeset 39438 c5ece2a7a86e
parent 39437 8c23c61c6d5c
child 39439 1c294d150ded
Isar "default" step needs to fail for solved problems, for clear distinction of '.' and '..' for example -- amending lapse introduced in 9de4d64eee3b (April 2004);
src/HOL/Power.thy file | annotate | diff | comparison | revisions
src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy file | annotate | diff | comparison | revisions
src/Pure/Isar/class.ML file | annotate | diff | comparison | revisions 
--- a/src/HOL/Power.thy	Thu Sep 16 15:32:24 2010 +0200
+++ b/src/HOL/Power.thy	Thu Sep 16 15:37:12 2010 +0200
@@ -29,7 +29,7 @@
 context monoid_mult
 begin
 
-subclass power ..
+subclass power .
 
 lemma power_one [simp]:
   "1 ^ n = 1"
--- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy	Thu Sep 16 15:32:24 2010 +0200
+++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy	Thu Sep 16 15:37:12 2010 +0200
@@ -791,7 +791,7 @@
     "k < l \<Longrightarrow> divmod_rel k l 0 k"
   | "k \<ge> l \<Longrightarrow> divmod_rel (k - l) l q r \<Longrightarrow> divmod_rel k l (Suc q) r"
 
-code_pred divmod_rel ..
+code_pred divmod_rel .
 thm divmod_rel.equation
 value [code] "Predicate.the (divmod_rel_i_i_o_o 1705 42)"
 
--- a/src/Pure/Isar/class.ML	Thu Sep 16 15:32:24 2010 +0200
+++ b/src/Pure/Isar/class.ML	Thu Sep 16 15:37:12 2010 +0200
@@ -630,7 +630,8 @@
   end;
 
 fun default_intro_tac ctxt [] =
-      intro_classes_tac [] ORELSE Locale.intro_locales_tac true ctxt []
+      COND Thm.no_prems no_tac
+        (intro_classes_tac [] ORELSE Locale.intro_locales_tac true ctxt [])
   | default_intro_tac _ _ = no_tac;
 
 fun default_tac rules ctxt facts =
isabelle