--- a/src/HOL/Decision_Procs/MIR.thy Tue Nov 27 19:31:11 2012 +0100
+++ b/src/HOL/Decision_Procs/MIR.thy Tue Nov 27 19:43:00 2012 +0100
@@ -5010,7 +5010,7 @@
from alluopairs_set1[where xs="?U"] have UpU: "set ?Up \<le> (set ?U \<times> set ?U)" by simp
from \<Upsilon>_l[OF lq] have U_l: "\<forall> (t,n) \<in> set ?U. numbound0 t \<and> n > 0" .
from U_l UpU
- have Up_: "\<forall> ((t,n),(s,m)) \<in> set ?Up. numbound0 t \<and> n> 0 \<and> numbound0 s \<and> m > 0" by auto
+ have "\<forall> ((t,n),(s,m)) \<in> set ?Up. numbound0 t \<and> n> 0 \<and> numbound0 s \<and> m > 0" by auto
hence Snb: "\<forall> (t,n) \<in> set ?S. numbound0 t \<and> n > 0 "
by (auto simp add: mult_pos_pos)
have Y_l: "\<forall> (t,n) \<in> set ?Y. numbound0 t \<and> n > 0"
--- a/src/HOL/Multivariate_Analysis/Integration.thy Tue Nov 27 19:31:11 2012 +0100
+++ b/src/HOL/Multivariate_Analysis/Integration.thy Tue Nov 27 19:43:00 2012 +0100
@@ -996,9 +996,9 @@
thus ?thesis apply- apply(rule that[of q]) unfolding True by auto next
case False note p = division_ofD[OF assms(1)]
have *:"\<forall>k\<in>p. \<exists>q. q division_of {a..b} \<and> k\<in>q" proof case goal1
- guess c using p(4)[OF goal1] .. then guess d .. note cd_ = this
- have *:"{c..d} \<subseteq> {a..b}" "{c..d} \<noteq> {}" using p(2,3)[OF goal1, unfolded cd_] using assms(2) by auto
- guess q apply(rule partial_division_extend_1[OF *]) . thus ?case unfolding cd_ by auto qed
+ guess c using p(4)[OF goal1] .. then guess d .. note "cd" = this
+ have *:"{c..d} \<subseteq> {a..b}" "{c..d} \<noteq> {}" using p(2,3)[OF goal1, unfolded "cd"] using assms(2) by auto
+ guess q apply(rule partial_division_extend_1[OF *]) . thus ?case unfolding "cd" by auto qed
guess q using bchoice[OF *] .. note q = conjunctD2[OF this[rule_format]]
have "\<And>x. x\<in>p \<Longrightarrow> \<exists>d. d division_of \<Union>(q x - {x})" apply(rule,rule_tac p="q x" in division_of_subset) proof-
fix x assume x:"x\<in>p" show "q x division_of \<Union>q x" apply-apply(rule division_ofI)
--- a/src/HOL/Proofs/Lambda/StrongNorm.thy Tue Nov 27 19:31:11 2012 +0100
+++ b/src/HOL/Proofs/Lambda/StrongNorm.thy Tue Nov 27 19:43:00 2012 +0100
@@ -102,7 +102,7 @@
assume uIT: "IT u"
assume uT: "e \<turnstile> u : T"
{
- case (Var rs n e_ T'_ u_ i_)
+ case (Var rs n e1 T'1 u1 i1)
assume nT: "e\<langle>i:T\<rangle> \<turnstile> Var n \<degree>\<degree> rs : T'"
let ?ty = "\<lambda>t. \<exists>T'. e\<langle>i:T\<rangle> \<turnstile> t : T'"
let ?R = "\<lambda>t. \<forall>e T' u i.
@@ -210,13 +210,13 @@
with False show ?thesis by (auto simp add: subst_Var)
qed
next
- case (Lambda r e_ T'_ u_ i_)
+ case (Lambda r e1 T'1 u1 i1)
assume "e\<langle>i:T\<rangle> \<turnstile> Abs r : T'"
and "\<And>e T' u i. PROP ?Q r e T' u i T"
with uIT uT show "IT (Abs r[u/i])"
by fastforce
next
- case (Beta r a as e_ T'_ u_ i_)
+ case (Beta r a as e1 T'1 u1 i1)
assume T: "e\<langle>i:T\<rangle> \<turnstile> Abs r \<degree> a \<degree>\<degree> as : T'"
assume SI1: "\<And>e T' u i. PROP ?Q (r[a/0] \<degree>\<degree> as) e T' u i T"
assume SI2: "\<And>e T' u i. PROP ?Q a e T' u i T"
--- a/src/HOL/Proofs/Lambda/WeakNorm.thy Tue Nov 27 19:31:11 2012 +0100
+++ b/src/HOL/Proofs/Lambda/WeakNorm.thy Tue Nov 27 19:43:00 2012 +0100
@@ -76,7 +76,7 @@
proof induct
fix e T' u i assume uNF: "NF u" and uT: "e \<turnstile> u : T"
{
- case (App ts x e_ T'_ u_ i_)
+ case (App ts x e1 T'1 u1 i1)
assume "e\<langle>i:T\<rangle> \<turnstile> Var x \<degree>\<degree> ts : T'"
then obtain Us
where varT: "e\<langle>i:T\<rangle> \<turnstile> Var x : Us \<Rrightarrow> T'"
@@ -187,7 +187,7 @@
qed
qed
next
- case (Abs r e_ T'_ u_ i_)
+ case (Abs r e1 T'1 u1 i1)
assume absT: "e\<langle>i:T\<rangle> \<turnstile> Abs r : T'"
then obtain R S where "e\<langle>0:R\<rangle>\<langle>Suc i:T\<rangle> \<turnstile> r : S" by (rule abs_typeE) simp
moreover have "NF (lift u 0)" using `NF u` by (rule lift_NF)
--- a/src/Pure/General/symbol.ML Tue Nov 27 19:31:11 2012 +0100
+++ b/src/Pure/General/symbol.ML Tue Nov 27 19:43:00 2012 +0100
@@ -46,6 +46,7 @@
val decode: symbol -> sym
datatype kind = Letter | Digit | Quasi | Blank | Other
val kind: symbol -> kind
+ val is_letter_symbol: symbol -> bool
val is_letter: symbol -> bool
val is_digit: symbol -> bool
val is_quasi: symbol -> bool
@@ -236,8 +237,6 @@
(* standard symbol kinds *)
-datatype kind = Letter | Digit | Quasi | Blank | Other;
-
local
val letter_symbols =
Symtab.make_set [
@@ -383,16 +382,22 @@
"\\<^isup>"
];
in
- fun kind s =
- if is_ascii_letter s then Letter
- else if is_ascii_digit s then Digit
- else if is_ascii_quasi s then Quasi
- else if is_ascii_blank s then Blank
- else if is_char s then Other
- else if Symtab.defined letter_symbols s then Letter
- else Other;
+
+val is_letter_symbol = Symtab.defined letter_symbols;
+
end;
+datatype kind = Letter | Digit | Quasi | Blank | Other;
+
+fun kind s =
+ if is_ascii_letter s then Letter
+ else if is_ascii_digit s then Digit
+ else if is_ascii_quasi s then Quasi
+ else if is_ascii_blank s then Blank
+ else if is_char s then Other
+ else if is_letter_symbol s then Letter
+ else Other;
+
fun is_letter s = kind s = Letter;
fun is_digit s = kind s = Digit;
fun is_quasi s = kind s = Quasi;
@@ -513,7 +518,8 @@
(* bump string -- treat as base 26 or base 1 numbers *)
-fun symbolic_end (_ :: "\\<^isub>" :: _) = true
+fun symbolic_end (_ :: "\\<^sub>" :: _) = true
+ | symbolic_end (_ :: "\\<^isub>" :: _) = true
| symbolic_end (_ :: "\\<^isup>" :: _) = true
| symbolic_end (s :: _) = is_symbolic s
| symbolic_end [] = false;
--- a/src/Pure/General/symbol_pos.ML Tue Nov 27 19:31:11 2012 +0100
+++ b/src/Pure/General/symbol_pos.ML Tue Nov 27 19:43:00 2012 +0100
@@ -37,8 +37,8 @@
val range: T list -> Position.range
val implode_range: Position.T -> Position.T -> T list -> text * Position.range
val explode: text * Position.T -> T list
+ val scan_new_ident: T list -> T list * T list
val scan_ident: T list -> T list * T list
- val is_ident: T list -> bool
val is_identifier: string -> bool
end;
@@ -214,6 +214,40 @@
(* identifiers *)
+local
+
+val latin = Symbol.is_ascii_letter;
+val digit = Symbol.is_ascii_digit;
+fun underscore s = s = "_";
+fun prime s = s = "'";
+fun script s = s = "\\<^sub>" orelse s = "\\<^isub>" orelse s = "\\<^isup>";
+fun special_letter s = Symbol.is_letter_symbol s andalso not (script s);
+
+val scan_plain = Scan.one ((latin orf digit orf prime) o symbol) >> single;
+val scan_digit = Scan.one (digit o symbol) >> single;
+val scan_prime = Scan.one (prime o symbol) >> single;
+
+val scan_script =
+ Scan.one (script o symbol) -- Scan.one ((latin orf digit orf special_letter) o symbol)
+ >> (fn (x, y) => [x, y]);
+
+val scan_ident_part1 =
+ Scan.one (latin o symbol) ::: (Scan.repeat (scan_plain || scan_script) >> flat) ||
+ Scan.one (special_letter o symbol) :::
+ (Scan.repeat (scan_digit || scan_prime || scan_script) >> flat);
+
+val scan_ident_part2 =
+ Scan.repeat1 (scan_plain || scan_script) >> flat ||
+ scan_ident_part1;
+
+in
+
+val scan_new_ident =
+ scan_ident_part1 @@@
+ (Scan.repeat (Scan.many1 (underscore o symbol) @@@ scan_ident_part2) >> flat);
+
+end;
+
val scan_ident =
Scan.one (Symbol.is_letter o symbol) ::: Scan.many (Symbol.is_letdig o symbol);
--- a/src/Pure/Syntax/lexicon.ML Tue Nov 27 19:31:11 2012 +0100
+++ b/src/Pure/Syntax/lexicon.ML Tue Nov 27 19:43:00 2012 +0100
@@ -293,6 +293,7 @@
fun idxname cs ds = (implode (rev cs), nat 0 ds);
fun chop_idx [] ds = idxname [] ds
+ | chop_idx (cs as (_ :: "\\<^sub>" :: _)) ds = idxname cs ds
| chop_idx (cs as (_ :: "\\<^isub>" :: _)) ds = idxname cs ds
| chop_idx (cs as (_ :: "\\<^isup>" :: _)) ds = idxname cs ds
| chop_idx (c :: cs) ds =
--- a/src/Pure/term.ML Tue Nov 27 19:31:11 2012 +0100
+++ b/src/Pure/term.ML Tue Nov 27 19:43:00 2012 +0100
@@ -981,7 +981,8 @@
val idx = string_of_int i;
val dot =
(case rev (Symbol.explode x) of
- _ :: "\\<^isub>" :: _ => false
+ _ :: "\\<^sub>" :: _ => false
+ | _ :: "\\<^isub>" :: _ => false
| _ :: "\\<^isup>" :: _ => false
| c :: _ => Symbol.is_digit c
| _ => true);