Mercurial Mercurial > wneuper > isa / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | bz2 | gz | help
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 39747c5ece2a7a86e
parent 39746 8c23c61c6d5c
child 39748 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 
     1.1 --- a/src/HOL/Power.thy	Thu Sep 16 15:32:24 2010 +0200
     1.2 +++ b/src/HOL/Power.thy	Thu Sep 16 15:37:12 2010 +0200
     1.3 @@ -29,7 +29,7 @@
     1.4  context monoid_mult
     1.5  begin
     1.6  
     1.7 -subclass power ..
     1.8 +subclass power .
     1.9  
    1.10  lemma power_one [simp]:
    1.11    "1 ^ n = 1"

     2.1 --- a/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy	Thu Sep 16 15:32:24 2010 +0200
     2.2 +++ b/src/HOL/Predicate_Compile_Examples/Predicate_Compile_Examples.thy	Thu Sep 16 15:37:12 2010 +0200
     2.3 @@ -791,7 +791,7 @@
     2.4      "k < l \<Longrightarrow> divmod_rel k l 0 k"
     2.5    | "k \<ge> l \<Longrightarrow> divmod_rel (k - l) l q r \<Longrightarrow> divmod_rel k l (Suc q) r"
     2.6  
     2.7 -code_pred divmod_rel ..
     2.8 +code_pred divmod_rel .
     2.9  thm divmod_rel.equation
    2.10  value [code] "Predicate.the (divmod_rel_i_i_o_o 1705 42)"
    2.11  

     3.1 --- a/src/Pure/Isar/class.ML	Thu Sep 16 15:32:24 2010 +0200
     3.2 +++ b/src/Pure/Isar/class.ML	Thu Sep 16 15:37:12 2010 +0200
     3.3 @@ -630,7 +630,8 @@
     3.4    end;
     3.5  
     3.6  fun default_intro_tac ctxt [] =
     3.7 -      intro_classes_tac [] ORELSE Locale.intro_locales_tac true ctxt []
     3.8 +      COND Thm.no_prems no_tac
     3.9 +        (intro_classes_tac [] ORELSE Locale.intro_locales_tac true ctxt [])
    3.10    | default_intro_tac _ _ = no_tac;
    3.11  
    3.12  fun default_tac rules ctxt facts =
wneuper/isa