--- a/src/CCL/Set.thy Mon Feb 08 21:26:52 2010 +0100
+++ b/src/CCL/Set.thy Mon Feb 08 21:28:27 2010 +0100
@@ -40,11 +40,11 @@
"@Bex" :: "[idt, 'a set, o] => o" ("(EX _:_./ _)" [0, 0, 0] 10)
translations
- "{x. P}" == "Collect(%x. P)"
- "INT x:A. B" == "INTER(A, %x. B)"
- "UN x:A. B" == "UNION(A, %x. B)"
- "ALL x:A. P" == "Ball(A, %x. P)"
- "EX x:A. P" == "Bex(A, %x. P)"
+ "{x. P}" == "CONST Collect(%x. P)"
+ "INT x:A. B" == "CONST INTER(A, %x. B)"
+ "UN x:A. B" == "CONST UNION(A, %x. B)"
+ "ALL x:A. P" == "CONST Ball(A, %x. P)"
+ "EX x:A. P" == "CONST Bex(A, %x. P)"
local
--- a/src/CCL/Type.thy Mon Feb 08 21:26:52 2010 +0100
+++ b/src/CCL/Type.thy Mon Feb 08 21:28:27 2010 +0100
@@ -39,15 +39,15 @@
"@Subtype" :: "[idt, 'a set, o] => 'a set" ("(1{_: _ ./ _})")
translations
- "PROD x:A. B" => "Pi(A, %x. B)"
- "A -> B" => "Pi(A, %_. B)"
- "SUM x:A. B" => "Sigma(A, %x. B)"
- "A * B" => "Sigma(A, %_. B)"
- "{x: A. B}" == "Subtype(A, %x. B)"
+ "PROD x:A. B" => "CONST Pi(A, %x. B)"
+ "A -> B" => "CONST Pi(A, %_. B)"
+ "SUM x:A. B" => "CONST Sigma(A, %x. B)"
+ "A * B" => "CONST Sigma(A, %_. B)"
+ "{x: A. B}" == "CONST Subtype(A, %x. B)"
print_translation {*
- [("Pi", dependent_tr' ("@Pi", "@->")),
- ("Sigma", dependent_tr' ("@Sigma", "@*"))] *}
+ [(@{const_syntax Pi}, dependent_tr' ("@Pi", "@->")),
+ (@{const_syntax Sigma}, dependent_tr' ("@Sigma", "@*"))] *}
axioms
Subtype_def: "{x:A. P(x)} == {x. x:A & P(x)}"
--- a/src/CTT/CTT.thy Mon Feb 08 21:26:52 2010 +0100
+++ b/src/CTT/CTT.thy Mon Feb 08 21:28:27 2010 +0100
@@ -63,8 +63,8 @@
"_PROD" :: "[idt,t,t]=>t" ("(3PROD _:_./ _)" 10)
"_SUM" :: "[idt,t,t]=>t" ("(3SUM _:_./ _)" 10)
translations
- "PROD x:A. B" == "Prod(A, %x. B)"
- "SUM x:A. B" == "Sum(A, %x. B)"
+ "PROD x:A. B" == "CONST Prod(A, %x. B)"
+ "SUM x:A. B" == "CONST Sum(A, %x. B)"
abbreviation
Arrow :: "[t,t]=>t" (infixr "-->" 30) where
--- a/src/Cube/Cube.thy Mon Feb 08 21:26:52 2010 +0100
+++ b/src/Cube/Cube.thy Mon Feb 08 21:28:27 2010 +0100
@@ -43,9 +43,9 @@
translations
("prop") "x:X" == ("prop") "|- x:X"
- "Lam x:A. B" == "Abs(A, %x. B)"
- "Pi x:A. B" => "Prod(A, %x. B)"
- "A -> B" => "Prod(A, %_. B)"
+ "Lam x:A. B" == "CONST Abs(A, %x. B)"
+ "Pi x:A. B" => "CONST Prod(A, %x. B)"
+ "A -> B" => "CONST Prod(A, %_. B)"
syntax (xsymbols)
Trueprop :: "[context', typing'] => prop" ("(_/ \<turnstile> _)")
@@ -54,7 +54,7 @@
Pi :: "[idt, term, term] => term" ("(3\<Pi> _:_./ _)" [0, 0] 10)
arrow :: "[term, term] => term" (infixr "\<rightarrow>" 10)
-print_translation {* [("Prod", dependent_tr' ("Pi", "arrow"))] *}
+print_translation {* [(@{const_syntax Prod}, dependent_tr' ("Pi", "arrow"))] *}
axioms
s_b: "*: []"
--- a/src/FOL/IFOL.thy Mon Feb 08 21:26:52 2010 +0100
+++ b/src/FOL/IFOL.thy Mon Feb 08 21:28:27 2010 +0100
@@ -772,7 +772,7 @@
translations
"_Let(_binds(b, bs), e)" == "_Let(b, _Let(bs, e))"
- "let x = a in e" == "Let(a, %x. e)"
+ "let x = a in e" == "CONST Let(a, %x. e)"
lemma LetI:
--- a/src/HOL/Algebra/FiniteProduct.thy Mon Feb 08 21:26:52 2010 +0100
+++ b/src/HOL/Algebra/FiniteProduct.thy Mon Feb 08 21:28:27 2010 +0100
@@ -302,7 +302,7 @@
"_finprod" :: "index => idt => 'a set => 'b => 'b"
("(3\<Otimes>__\<in>_. _)" [1000, 0, 51, 10] 10)
translations
- "\<Otimes>\<index>i:A. b" == "finprod \<struct>\<index> (%i. b) A"
+ "\<Otimes>\<index>i:A. b" == "CONST finprod \<struct>\<index> (%i. b) A"
-- {* Beware of argument permutation! *}
lemma (in comm_monoid) finprod_empty [simp]:
--- a/src/HOL/Algebra/Ring.thy Mon Feb 08 21:26:52 2010 +0100
+++ b/src/HOL/Algebra/Ring.thy Mon Feb 08 21:28:27 2010 +0100
@@ -213,7 +213,7 @@
"_finsum" :: "index => idt => 'a set => 'b => 'b"
("(3\<Oplus>__\<in>_. _)" [1000, 0, 51, 10] 10)
translations
- "\<Oplus>\<index>i:A. b" == "finsum \<struct>\<index> (%i. b) A"
+ "\<Oplus>\<index>i:A. b" == "CONST finsum \<struct>\<index> (%i. b) A"
-- {* Beware of argument permutation! *}
context abelian_monoid begin
--- a/src/HOL/Auth/Message.thy Mon Feb 08 21:26:52 2010 +0100
+++ b/src/HOL/Auth/Message.thy Mon Feb 08 21:28:27 2010 +0100
@@ -58,7 +58,7 @@
translations
"{|x, y, z|}" == "{|x, {|y, z|}|}"
- "{|x, y|}" == "MPair x y"
+ "{|x, y|}" == "CONST MPair x y"
constdefs
--- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Mon Feb 08 21:26:52 2010 +0100
+++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Mon Feb 08 21:28:27 2010 +0100
@@ -15,11 +15,8 @@
datatype poly = C Num| Bound nat| Add poly poly|Sub poly poly
| Mul poly poly| Neg poly| Pw poly nat| CN poly nat poly
-ML{* @{term "Add"}*}
-syntax "_poly0" :: "poly" ("0\<^sub>p")
-translations "0\<^sub>p" \<rightleftharpoons> "C (0\<^sub>N)"
-syntax "_poly" :: "int \<Rightarrow> poly" ("_\<^sub>p")
-translations "i\<^sub>p" \<rightleftharpoons> "C (i\<^sub>N)"
+abbreviation poly_0 :: "poly" ("0\<^sub>p") where "0\<^sub>p \<equiv> C (0\<^sub>N)"
+abbreviation poly_p :: "int \<Rightarrow> poly" ("_\<^sub>p") where "i\<^sub>p \<equiv> C (i\<^sub>N)"
subsection{* Boundedness, substitution and all that *}
consts polysize:: "poly \<Rightarrow> nat"
@@ -117,14 +114,14 @@
polysub :: "poly\<times>poly \<Rightarrow> poly"
polymul :: "poly\<times>poly \<Rightarrow> poly"
polypow :: "nat \<Rightarrow> poly \<Rightarrow> poly"
-syntax "_polyadd" :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "+\<^sub>p" 60)
-translations "a +\<^sub>p b" \<rightleftharpoons> "polyadd (a,b)"
-syntax "_polymul" :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "*\<^sub>p" 60)
-translations "a *\<^sub>p b" \<rightleftharpoons> "polymul (a,b)"
-syntax "_polysub" :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "-\<^sub>p" 60)
-translations "a -\<^sub>p b" \<rightleftharpoons> "polysub (a,b)"
-syntax "_polypow" :: "nat \<Rightarrow> poly \<Rightarrow> poly" (infixl "^\<^sub>p" 60)
-translations "a ^\<^sub>p k" \<rightleftharpoons> "polypow k a"
+abbreviation poly_add :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "+\<^sub>p" 60)
+ where "a +\<^sub>p b \<equiv> polyadd (a,b)"
+abbreviation poly_mul :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "*\<^sub>p" 60)
+ where "a *\<^sub>p b \<equiv> polymul (a,b)"
+abbreviation poly_sub :: "poly \<Rightarrow> poly \<Rightarrow> poly" (infixl "-\<^sub>p" 60)
+ where "a -\<^sub>p b \<equiv> polysub (a,b)"
+abbreviation poly_pow :: "poly \<Rightarrow> nat \<Rightarrow> poly" (infixl "^\<^sub>p" 60)
+ where "a ^\<^sub>p k \<equiv> polypow k a"
recdef polyadd "measure (\<lambda> (a,b). polysize a + polysize b)"
"polyadd (C c, C c') = C (c+\<^sub>Nc')"
@@ -243,8 +240,9 @@
"Ipoly bs (Mul a b) = Ipoly bs a * Ipoly bs b"
"Ipoly bs (Pw t n) = (Ipoly bs t) ^ n"
"Ipoly bs (CN c n p) = (Ipoly bs c) + (bs!n)*(Ipoly bs p)"
-syntax "_Ipoly" :: "poly \<Rightarrow> 'a list \<Rightarrow>'a::{ring_char_0,power,division_by_zero,field}" ("\<lparr>_\<rparr>\<^sub>p\<^bsup>_\<^esup>")
-translations "\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup>" \<rightleftharpoons> "Ipoly bs p"
+abbreviation
+ Ipoly_syntax :: "poly \<Rightarrow> 'a list \<Rightarrow>'a::{ring_char_0,power,division_by_zero,field}" ("\<lparr>_\<rparr>\<^sub>p\<^bsup>_\<^esup>")
+ where "\<lparr>p\<rparr>\<^sub>p\<^bsup>bs\<^esup> \<equiv> Ipoly bs p"
lemma Ipoly_CInt: "Ipoly bs (C (i,1)) = of_int i"
by (simp add: INum_def)
--- a/src/HOL/Hoare/Hoare.thy Mon Feb 08 21:26:52 2010 +0100
+++ b/src/HOL/Hoare/Hoare.thy Mon Feb 08 21:28:27 2010 +0100
@@ -24,12 +24,7 @@
| Cond "'a bexp" "'a com" "'a com" ("(1IF _/ THEN _ / ELSE _/ FI)" [0,0,0] 61)
| While "'a bexp" "'a assn" "'a com" ("(1WHILE _/ INV {_} //DO _ /OD)" [0,0,0] 61)
-syntax
- "@assign" :: "id => 'b => 'a com" ("(2_ :=/ _)" [70,65] 61)
- "@annskip" :: "'a com" ("SKIP")
-
-translations
- "SKIP" == "Basic id"
+abbreviation annskip ("SKIP") where "SKIP == Basic id"
types 'a sem = "'a => 'a => bool"
@@ -50,16 +45,19 @@
"Valid p c q == !s s'. Sem c s s' --> s : p --> s' : q"
-syntax
- "@hoare_vars" :: "[idts, 'a assn,'a com,'a assn] => bool"
- ("VARS _// {_} // _ // {_}" [0,0,55,0] 50)
-syntax ("" output)
- "@hoare" :: "['a assn,'a com,'a assn] => bool"
- ("{_} // _ // {_}" [0,55,0] 50)
(** parse translations **)
-ML{*
+syntax
+ "_assign" :: "id => 'b => 'a com" ("(2_ :=/ _)" [70,65] 61)
+
+syntax
+ "_hoare_vars" :: "[idts, 'a assn,'a com,'a assn] => bool"
+ ("VARS _// {_} // _ // {_}" [0,0,55,0] 50)
+syntax ("" output)
+ "_hoare" :: "['a assn,'a com,'a assn] => bool"
+ ("{_} // _ // {_}" [0,55,0] 50)
+ML {*
local
@@ -91,7 +89,7 @@
*}
(* com_tr *)
ML{*
-fun com_tr (Const("@assign",_) $ Free (a,_) $ e) xs =
+fun com_tr (Const("_assign",_) $ Free (a,_) $ e) xs =
Syntax.const "Basic" $ mk_fexp a e xs
| com_tr (Const ("Basic",_) $ f) xs = Syntax.const "Basic" $ f
| com_tr (Const ("Seq",_) $ c1 $ c2) xs =
@@ -123,7 +121,7 @@
end
*}
-parse_translation {* [("@hoare_vars", hoare_vars_tr)] *}
+parse_translation {* [("_hoare_vars", hoare_vars_tr)] *}
(*****************************************************************************)
@@ -175,8 +173,8 @@
fun mk_assign f =
let val (vs, ts) = mk_vts f;
val (ch, which) = find_ch (vs~~ts) ((length vs)-1) (rev vs)
- in if ch then Syntax.const "@assign" $ fst(which) $ snd(which)
- else Syntax.const "@skip" end;
+ in if ch then Syntax.const "_assign" $ fst(which) $ snd(which)
+ else Syntax.const @{const_syntax annskip} end;
fun com_tr' (Const ("Basic",_) $ f) = if is_f f then mk_assign f
else Syntax.const "Basic" $ f
@@ -190,10 +188,10 @@
fun spec_tr' [p, c, q] =
- Syntax.const "@hoare" $ assn_tr' p $ com_tr' c $ assn_tr' q
+ Syntax.const "_hoare" $ assn_tr' p $ com_tr' c $ assn_tr' q
*}
-print_translation {* [("Valid", spec_tr')] *}
+print_translation {* [(@{const_syntax Valid}, spec_tr')] *}
lemma SkipRule: "p \<subseteq> q \<Longrightarrow> Valid p (Basic id) q"
by (auto simp:Valid_def)
--- a/src/HOL/Hoare/HoareAbort.thy Mon Feb 08 21:26:52 2010 +0100
+++ b/src/HOL/Hoare/HoareAbort.thy Mon Feb 08 21:28:27 2010 +0100
@@ -21,12 +21,7 @@
| Cond "'a bexp" "'a com" "'a com" ("(1IF _/ THEN _ / ELSE _/ FI)" [0,0,0] 61)
| While "'a bexp" "'a assn" "'a com" ("(1WHILE _/ INV {_} //DO _ /OD)" [0,0,0] 61)
-syntax
- "@assign" :: "id => 'b => 'a com" ("(2_ :=/ _)" [70,65] 61)
- "@annskip" :: "'a com" ("SKIP")
-
-translations
- "SKIP" == "Basic id"
+abbreviation annskip ("SKIP") where "SKIP == Basic id"
types 'a sem = "'a option => 'a option => bool"
@@ -51,16 +46,19 @@
"Valid p c q == \<forall>s s'. Sem c s s' \<longrightarrow> s : Some ` p \<longrightarrow> s' : Some ` q"
-syntax
- "@hoare_vars" :: "[idts, 'a assn,'a com,'a assn] => bool"
- ("VARS _// {_} // _ // {_}" [0,0,55,0] 50)
-syntax ("" output)
- "@hoare" :: "['a assn,'a com,'a assn] => bool"
- ("{_} // _ // {_}" [0,55,0] 50)
(** parse translations **)
-ML{*
+syntax
+ "_assign" :: "id => 'b => 'a com" ("(2_ :=/ _)" [70,65] 61)
+
+syntax
+ "_hoare_vars" :: "[idts, 'a assn,'a com,'a assn] => bool"
+ ("VARS _// {_} // _ // {_}" [0,0,55,0] 50)
+syntax ("" output)
+ "_hoare" :: "['a assn,'a com,'a assn] => bool"
+ ("{_} // _ // {_}" [0,55,0] 50)
+ML {*
local
fun free a = Free(a,dummyT)
@@ -92,7 +90,7 @@
*}
(* com_tr *)
ML{*
-fun com_tr (Const("@assign",_) $ Free (a,_) $ e) xs =
+fun com_tr (Const("_assign",_) $ Free (a,_) $ e) xs =
Syntax.const "Basic" $ mk_fexp a e xs
| com_tr (Const ("Basic",_) $ f) xs = Syntax.const "Basic" $ f
| com_tr (Const ("Seq",_) $ c1 $ c2) xs =
@@ -124,7 +122,7 @@
end
*}
-parse_translation {* [("@hoare_vars", hoare_vars_tr)] *}
+parse_translation {* [("_hoare_vars", hoare_vars_tr)] *}
(*****************************************************************************)
@@ -176,8 +174,8 @@
fun mk_assign f =
let val (vs, ts) = mk_vts f;
val (ch, which) = find_ch (vs~~ts) ((length vs)-1) (rev vs)
- in if ch then Syntax.const "@assign" $ fst(which) $ snd(which)
- else Syntax.const "@skip" end;
+ in if ch then Syntax.const "_assign" $ fst(which) $ snd(which)
+ else Syntax.const @{const_syntax annskip} end;
fun com_tr' (Const ("Basic",_) $ f) = if is_f f then mk_assign f
else Syntax.const "Basic" $ f
@@ -191,10 +189,10 @@
fun spec_tr' [p, c, q] =
- Syntax.const "@hoare" $ assn_tr' p $ com_tr' c $ assn_tr' q
+ Syntax.const "_hoare" $ assn_tr' p $ com_tr' c $ assn_tr' q
*}
-print_translation {* [("Valid", spec_tr')] *}
+print_translation {* [(@{const_syntax Valid}, spec_tr')] *}
(*** The proof rules ***)
@@ -257,7 +255,7 @@
syntax
guarded_com :: "bool \<Rightarrow> 'a com \<Rightarrow> 'a com" ("(2_ \<rightarrow>/ _)" 71)
- array_update :: "'a list \<Rightarrow> nat \<Rightarrow> 'a \<Rightarrow> 'a com" ("(2_[_] :=/ _)" [70,65] 61)
+ 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 < CONST length a) \<rightarrow> (a := CONST list_update a i v)"
--- a/src/HOL/Isar_Examples/Hoare.thy Mon Feb 08 21:26:52 2010 +0100
+++ b/src/HOL/Isar_Examples/Hoare.thy Mon Feb 08 21:28:27 2010 +0100
@@ -228,11 +228,11 @@
"_Assert" :: "'a => 'a set" ("(\<lbrace>_\<rbrace>)" [0] 1000)
translations
- ".{b}." => "Collect .(b)."
+ ".{b}." => "CONST Collect .(b)."
"B [a/\<acute>x]" => ".{\<acute>(_update_name x (\<lambda>_. a)) \<in> B}."
- "\<acute>x := a" => "Basic .(\<acute>(_update_name x (\<lambda>_. a)))."
- "IF b THEN c1 ELSE c2 FI" => "Cond .{b}. c1 c2"
- "WHILE b INV i DO c OD" => "While .{b}. i c"
+ "\<acute>x := a" => "CONST Basic .(\<acute>(_update_name x (\<lambda>_. a)))."
+ "IF b THEN c1 ELSE c2 FI" => "CONST Cond .{b}. c1 c2"
+ "WHILE b INV i DO c OD" => "CONST While .{b}. i c"
"WHILE b DO c OD" == "WHILE b INV CONST undefined DO c OD"
parse_translation {*
--- a/src/HOL/Metis_Examples/Message.thy Mon Feb 08 21:26:52 2010 +0100
+++ b/src/HOL/Metis_Examples/Message.thy Mon Feb 08 21:28:27 2010 +0100
@@ -52,7 +52,7 @@
translations
"{|x, y, z|}" == "{|x, {|y, z|}|}"
- "{|x, y|}" == "MPair x y"
+ "{|x, y|}" == "CONST MPair x y"
constdefs
--- a/src/HOL/Metis_Examples/Tarski.thy Mon Feb 08 21:26:52 2010 +0100
+++ b/src/HOL/Metis_Examples/Tarski.thy Mon Feb 08 21:28:27 2010 +0100
@@ -78,11 +78,9 @@
{S. S \<subseteq> pset cl &
(| pset = S, order = induced S (order cl) |): CompleteLattice }"
-syntax
- "@SL" :: "['a set, 'a potype] => bool" ("_ <<= _" [51,50]50)
-
-translations
- "S <<= cl" == "S : sublattice `` {cl}"
+abbreviation
+ sublattice_syntax :: "['a set, 'a potype] => bool" ("_ <<= _" [51, 50] 50)
+ where "S <<= cl \<equiv> S : sublattice `` {cl}"
constdefs
dual :: "'a potype => 'a potype"
--- a/src/HOL/Number_Theory/UniqueFactorization.thy Mon Feb 08 21:26:52 2010 +0100
+++ b/src/HOL/Number_Theory/UniqueFactorization.thy Mon Feb 08 21:28:27 2010 +0100
@@ -76,7 +76,7 @@
("(3PROD _:#_. _)" [0, 51, 10] 10)
translations
- "PROD i :# A. b" == "msetprod (%i. b) A"
+ "PROD i :# A. b" == "CONST msetprod (%i. b) A"
lemma msetprod_Un: "msetprod f (A+B) = msetprod f A * msetprod f B"
apply (simp add: msetprod_def power_add)
--- a/src/HOL/UNITY/PPROD.thy Mon Feb 08 21:26:52 2010 +0100
+++ b/src/HOL/UNITY/PPROD.thy Mon Feb 08 21:28:27 2010 +0100
@@ -11,17 +11,14 @@
theory PPROD imports Lift_prog begin
constdefs
-
PLam :: "[nat set, nat => ('b * ((nat=>'b) * 'c)) program]
=> ((nat=>'b) * 'c) program"
"PLam I F == \<Squnion>i \<in> I. lift i (F i)"
syntax
- "@PLam" :: "[pttrn, nat set, 'b set] => (nat => 'b) set"
- ("(3plam _:_./ _)" 10)
-
+ "_PLam" :: "[pttrn, nat set, 'b set] => (nat => 'b) set" ("(3plam _:_./ _)" 10)
translations
- "plam x : A. B" == "PLam A (%x. B)"
+ "plam x : A. B" == "CONST PLam A (%x. B)"
(*** Basic properties ***)
--- a/src/HOL/UNITY/Union.thy Mon Feb 08 21:26:52 2010 +0100
+++ b/src/HOL/UNITY/Union.thy Mon Feb 08 21:28:27 2010 +0100
@@ -36,19 +36,19 @@
"safety_prop X == SKIP: X & (\<forall>G. Acts G \<subseteq> UNION X Acts --> G \<in> X)"
syntax
- "@JOIN1" :: "[pttrns, 'b set] => 'b set" ("(3JN _./ _)" 10)
- "@JOIN" :: "[pttrn, 'a set, 'b set] => 'b set" ("(3JN _:_./ _)" 10)
+ "_JOIN1" :: "[pttrns, 'b set] => 'b set" ("(3JN _./ _)" 10)
+ "_JOIN" :: "[pttrn, 'a set, 'b set] => 'b set" ("(3JN _:_./ _)" 10)
translations
- "JN x : A. B" == "JOIN A (%x. B)"
- "JN x y. B" == "JN x. JN y. B"
- "JN x. B" == "JOIN CONST UNIV (%x. B)"
+ "JN x: A. B" == "CONST JOIN A (%x. B)"
+ "JN x y. B" == "JN x. JN y. B"
+ "JN x. B" == "JOIN CONST UNIV (%x. B)"
syntax (xsymbols)
SKIP :: "'a program" ("\<bottom>")
Join :: "['a program, 'a program] => 'a program" (infixl "\<squnion>" 65)
- "@JOIN1" :: "[pttrns, 'b set] => 'b set" ("(3\<Squnion> _./ _)" 10)
- "@JOIN" :: "[pttrn, 'a set, 'b set] => 'b set" ("(3\<Squnion> _\<in>_./ _)" 10)
+ "_JOIN1" :: "[pttrns, 'b set] => 'b set" ("(3\<Squnion> _./ _)" 10)
+ "_JOIN" :: "[pttrn, 'a set, 'b set] => 'b set" ("(3\<Squnion> _\<in>_./ _)" 10)
subsection{*SKIP*}
--- a/src/Sequents/ILL_predlog.thy Mon Feb 08 21:26:52 2010 +0100
+++ b/src/Sequents/ILL_predlog.thy Mon Feb 08 21:28:27 2010 +0100
@@ -22,8 +22,8 @@
"[* A & B *]" == "[*A*] && [*B*]"
"[* A | B *]" == "![*A*] ++ ![*B*]"
- "[* - A *]" == "[*A > ff*]"
- "[* ff *]" == "0"
+ "[* - A *]" == "[*A > CONST ff*]"
+ "[* XCONST ff *]" == "0"
"[* A = B *]" => "[* (A > B) & (B > A) *]"
"[* A > B *]" == "![*A*] -o [*B*]"