--- a/src/HOL/Hoare/HoareAbort.thy Thu Sep 28 23:42:39 2006 +0200
+++ b/src/HOL/Hoare/HoareAbort.thy Thu Sep 28 23:42:43 2006 +0200
@@ -255,7 +255,7 @@
array_update :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a com" ("(2_[_] :=/ _)" [70,65] 61)
translations
"P \<rightarrow> c" == "IF P THEN c ELSE Abort FI"
- "a[i] := v" => "(i < length a) \<rightarrow> (a := list_update a i v)"
+ "a[i] := v" => "(i < CONST length a) \<rightarrow> (a := list_update a i v)"
(* reverse translation not possible because of duplicate "a" *)
text{* Note: there is no special syntax for guarded array access. Thus
--- a/src/HOL/Hyperreal/Series.thy Thu Sep 28 23:42:39 2006 +0200
+++ b/src/HOL/Hyperreal/Series.thy Thu Sep 28 23:42:43 2006 +0200
@@ -27,7 +27,7 @@
syntax
"_suminf" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a" ("\<Sum>_. _" [0, 10] 10)
translations
- "\<Sum>i. b" == "suminf (%i. b)"
+ "\<Sum>i. b" == "CONST suminf (%i. b)"
lemma sumr_diff_mult_const:
--- a/src/HOL/Induct/LList.thy Thu Sep 28 23:42:39 2006 +0200
+++ b/src/HOL/Induct/LList.thy Thu Sep 28 23:42:43 2006 +0200
@@ -95,8 +95,11 @@
text{* The case syntax for type @{text "'a llist"} *}
+syntax (* FIXME proper case syntax!? *)
+ LNil :: logic
+ LCons :: logic
translations
- "case p of LNil => a | LCons x l => b" == "llist_case a (%x l. b) p"
+ "case p of LNil => a | LCons x l => b" == "CONST llist_case a (%x l. b) p"
subsubsection{* Sample function definitions. Item-based ones start with @{text L} *}
--- a/src/HOL/Induct/SList.thy Thu Sep 28 23:42:39 2006 +0200
+++ b/src/HOL/Induct/SList.thy Thu Sep 28 23:42:43 2006 +0200
@@ -73,7 +73,7 @@
(*Declaring the abstract list constructors*)
definition
- Nil :: "'a list"
+ Nil :: "'a list" ("[]")
"Nil = Abs_List(NIL)"
"Cons" :: "['a, 'a list] => 'a list" (infixr "#" 65)
@@ -88,19 +88,16 @@
"list_case a f xs = list_rec xs a (%x xs r. f x xs)"
(* list Enumeration *)
-consts
- "[]" :: "'a list" ("[]")
syntax
"@list" :: "args => 'a list" ("[(_)]")
translations
"[x, xs]" == "x#[xs]"
"[x]" == "x#[]"
- "[]" == "Nil"
- "case xs of Nil => a | y#ys => b" == "list_case(a, %y ys. b, xs)"
+ "case xs of [] => a | y#ys => b" == "CONST list_case(a, %y ys. b, xs)"
-
+
(* *********************************************************************** *)
(* *)
(* Generalized Map Functionals *)
@@ -205,8 +202,8 @@
"@filter" :: "[idt, 'a list, bool] => 'a list" ("(1[_:_ ./ _])")
translations
- "[x:xs. P]" == "filter(%x. P) xs"
- "Alls x:xs. P"== "list_all(%x. P)xs"
+ "[x:xs. P]" == "CONST filter(%x. P) xs"
+ "Alls x:xs. P" == "CONST list_all(%x. P)xs"
lemma ListI: "x : list (range Leaf) ==> x : List"
--- a/src/HOL/Library/Coinductive_List.thy Thu Sep 28 23:42:39 2006 +0200
+++ b/src/HOL/Library/Coinductive_List.thy Thu Sep 28 23:42:43 2006 +0200
@@ -196,8 +196,12 @@
definition
"llist_case c d l =
List_case c (\<lambda>x y. d (inv Datatype_Universe.Leaf x) (Abs_llist y)) (Rep_llist l)"
+
+syntax (* FIXME? *)
+ LNil :: logic
+ LCons :: logic
translations
- "case p of LNil \<Rightarrow> a | LCons x l \<Rightarrow> b" \<rightleftharpoons> "llist_case a (\<lambda>x l. b) p"
+ "case p of LNil \<Rightarrow> a | LCons x l \<Rightarrow> b" \<rightleftharpoons> "CONST llist_case a (\<lambda>x l. b) p"
lemma llist_case_LNil [simp]: "llist_case c d LNil = c"
by (simp add: llist_case_def LNil_def
--- a/src/HOL/Library/FuncSet.thy Thu Sep 28 23:42:39 2006 +0200
+++ b/src/HOL/Library/FuncSet.thy Thu Sep 28 23:42:43 2006 +0200
@@ -39,8 +39,8 @@
"_lam" :: "[pttrn, 'a set, 'a => 'b] => ('a=>'b)" ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
translations
- "PI x:A. B" == "Pi A (%x. B)"
- "%x:A. f" == "restrict (%x. f) A"
+ "PI x:A. B" == "CONST Pi A (%x. B)"
+ "%x:A. f" == "CONST restrict (%x. f) A"
definition
"compose" :: "['a set, 'b => 'c, 'a => 'b] => ('a => 'c)"
--- a/src/HOL/Library/Multiset.thy Thu Sep 28 23:42:39 2006 +0200
+++ b/src/HOL/Library/Multiset.thy Thu Sep 28 23:42:43 2006 +0200
@@ -40,7 +40,7 @@
syntax
"_MCollect" :: "pttrn => 'a multiset => bool => 'a multiset" ("(1{# _ : _./ _#})")
translations
- "{#x:M. P#}" == "MCollect M (\<lambda>x. P)"
+ "{#x:M. P#}" == "CONST MCollect M (\<lambda>x. P)"
definition
set_of :: "'a multiset => 'a set"
--- a/src/HOLCF/Porder.thy Thu Sep 28 23:42:39 2006 +0200
+++ b/src/HOLCF/Porder.thy Thu Sep 28 23:42:43 2006 +0200
@@ -94,7 +94,7 @@
"LUB " :: "[idts, 'a] \<Rightarrow> 'a" ("(3\<Squnion>_./ _)" [0,10] 10)
translations
- "\<Squnion>n. t" == "lub(range(\<lambda>n. t))"
+ "\<Squnion>n. t" == "lub(CONST range(\<lambda>n. t))"
text {* lubs are unique *}