--- a/doc/Contents Thu Mar 12 15:31:26 2009 +0100
+++ b/doc/Contents Thu Mar 12 15:31:44 2009 +0100
@@ -6,7 +6,7 @@
classes Tutorial on Type Classes
functions Tutorial on Function Definitions
codegen Tutorial on Code Generation
- sugar LaTeX sugar for proof documents
+ sugar LaTeX Sugar for Isabelle documents
Reference Manuals
isar-ref The Isabelle/Isar Reference Manual
--- a/src/HOL/IsaMakefile Thu Mar 12 15:31:26 2009 +0100
+++ b/src/HOL/IsaMakefile Thu Mar 12 15:31:44 2009 +0100
@@ -344,7 +344,8 @@
Library/Product_plus.thy \
Library/Product_Vector.thy \
Library/Enum.thy Library/Float.thy $(SRC)/Tools/float.ML $(SRC)/HOL/Tools/float_arith.ML \
- Library/reify_data.ML Library/reflection.ML
+ Library/reify_data.ML Library/reflection.ML \
+ Library/LaTeXsugar.thy Library/OptionalSugar.thy
@cd Library; $(ISABELLE_TOOL) usedir $(OUT)/HOL Library
--- a/src/HOL/Library/OptionalSugar.thy Thu Mar 12 15:31:26 2009 +0100
+++ b/src/HOL/Library/OptionalSugar.thy Thu Mar 12 15:31:44 2009 +0100
@@ -4,13 +4,21 @@
*)
(*<*)
theory OptionalSugar
-imports LaTeXsugar
+imports LaTeXsugar Complex_Main
begin
-(* set *)
+(* hiding set *)
translations
"xs" <= "CONST set xs"
+(* hiding numeric conversions - embeddings only *)
+translations
+ "n" <= "CONST of_nat n"
+ "n" <= "CONST int n"
+ "n" <= "real n"
+ "n" <= "CONST real_of_nat n"
+ "n" <= "CONST real_of_int n"
+
(* append *)
syntax (latex output)
"appendL" :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" (infixl "\<^raw:\isacharat>" 65)
--- a/src/Pure/General/binding.ML Thu Mar 12 15:31:26 2009 +0100
+++ b/src/Pure/General/binding.ML Thu Mar 12 15:31:44 2009 +0100
@@ -14,7 +14,7 @@
val make: bstring * Position.T -> binding
val pos_of: binding -> Position.T
val name: bstring -> binding
- val name_of: binding -> string
+ val name_of: binding -> bstring
val map_name: (bstring -> bstring) -> binding -> binding
val prefix_name: string -> binding -> binding
val suffix_name: string -> binding -> binding
@@ -22,8 +22,8 @@
val empty: binding
val is_empty: binding -> bool
val qualify: bool -> string -> binding -> binding
- val qualified_name: bstring -> binding
- val qualified_name_of: binding -> bstring
+ val qualified_name: string -> binding
+ val qualified_name_of: binding -> string
val prefix_of: binding -> (string * bool) list
val map_prefix: ((string * bool) list -> (string * bool) list) -> binding -> binding
val prefix: bool -> string -> binding -> binding
--- a/src/Pure/General/name_space.ML Thu Mar 12 15:31:26 2009 +0100
+++ b/src/Pure/General/name_space.ML Thu Mar 12 15:31:44 2009 +0100
@@ -36,13 +36,13 @@
val root_path: naming -> naming
val parent_path: naming -> naming
val no_base_names: naming -> naming
- val sticky_prefix: string -> naming -> naming
+ val mandatory_path: string -> naming -> naming
type 'a table = T * 'a Symtab.table
- val bind: naming -> binding * 'a -> 'a table -> string * 'a table (*exception Symtab.DUP*)
+ val define: naming -> binding * 'a -> 'a table -> string * 'a table (*exception Symtab.DUP*)
val empty_table: 'a table
- val merge_tables: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table (*exception Symtab.DUP*)
+ val merge_tables: ('a * 'a -> bool) -> 'a table * 'a table -> 'a table (*exception Symtab.DUP*)
val join_tables: (string -> 'a * 'a -> 'a) (*exception Symtab.DUP/Symtab.SAME*) ->
- 'a table * 'a table -> 'a table (*exception Symtab.DUP*)
+ 'a table * 'a table -> 'a table (*exception Symtab.DUP*)
val dest_table: 'a table -> (string * 'a) list
val extern_table: 'a table -> (xstring * 'a) list
end;
@@ -156,8 +156,8 @@
fun merge (NameSpace (tab1, xtab1), NameSpace (tab2, xtab2)) =
let
val tab' = (tab1, tab2) |> Symtab.join
- (K (fn names as ((names1, names1'), (names2, names2')) =>
- if pointer_eq names then raise Symtab.SAME
+ (K (fn ((names1, names1'), (names2, names2')) =>
+ if pointer_eq (names1, names2) andalso pointer_eq (names1', names2') then raise Symtab.SAME
else (Library.merge (op =) (names1, names2), Library.merge (op =) (names1', names2'))));
val xtab' = (xtab1, xtab2) |> Symtab.join
(K (fn xnames =>
@@ -187,22 +187,22 @@
val default_naming = make_naming ([], false);
fun add_path elems = map_naming (fn (path, no_base_names) =>
- (path @ map (rpair false) (Long_Name.explode elems), no_base_names));
+ (path @ [(elems, false)], no_base_names));
val root_path = map_naming (fn (_, no_base_names) => ([], no_base_names));
val parent_path = map_naming (fn (path, no_base_names) =>
(perhaps (try (#1 o split_last)) path, no_base_names));
-fun sticky_prefix elems = map_naming (fn (path, no_base_names) =>
- (path @ map (rpair true) (Long_Name.explode elems), no_base_names));
+fun mandatory_path elems = map_naming (fn (path, no_base_names) =>
+ (path @ [(elems, true)], no_base_names));
val no_base_names = map_naming (fn (path, _) => (path, true));
(* full name *)
-fun err_bad binding = error ("Bad name declaration " ^ quote (Binding.str_of binding));
+fun err_bad binding = error ("Bad name binding " ^ quote (Binding.str_of binding));
fun name_spec (Naming {path, ...}) binding =
let
@@ -230,7 +230,6 @@
| mandatory_prefixes1 ((x, true) :: xs) = map (cons x) (mandatory_prefixes1 xs)
| mandatory_prefixes1 ((x, false) :: xs) = map (cons x) (mandatory_prefixes xs);
-fun mandatory_suffixes1 xs = map rev (mandatory_prefixes1 (rev xs));
fun mandatory_suffixes xs = map rev (mandatory_prefixes (rev xs));
fun accesses (naming as Naming {no_base_names, ...}) binding =
@@ -264,7 +263,7 @@
type 'a table = T * 'a Symtab.table;
-fun bind naming (binding, x) (space, tab) =
+fun define naming (binding, x) (space, tab) =
let val (name, space') = declare naming binding space
in (name, (space', Symtab.update_new (name, x) tab)) end;
--- a/src/Pure/Isar/attrib.ML Thu Mar 12 15:31:26 2009 +0100
+++ b/src/Pure/Isar/attrib.ML Thu Mar 12 15:31:44 2009 +0100
@@ -146,7 +146,7 @@
let
val new_attrs =
raw_attrs |> map (fn (name, att, comment) => (Binding.name name, ((att, comment), stamp ())));
- fun add attrs = fold (snd oo NameSpace.bind (Sign.naming_of thy)) new_attrs attrs
+ fun add attrs = fold (snd oo NameSpace.define (Sign.naming_of thy)) new_attrs attrs
handle Symtab.DUP dup => error ("Duplicate declaration of attributes " ^ quote dup);
in Attributes.map add thy end;
--- a/src/Pure/Isar/expression.ML Thu Mar 12 15:31:26 2009 +0100
+++ b/src/Pure/Isar/expression.ML Thu Mar 12 15:31:44 2009 +0100
@@ -674,8 +674,7 @@
|> def_pred aname parms defs' exts exts';
val (_, thy'') =
thy'
- |> Sign.add_path (Binding.name_of aname)
- |> Sign.no_base_names
+ |> Sign.mandatory_path (Binding.name_of aname)
|> PureThy.note_thmss Thm.internalK
[((Binding.name introN, []), [([intro], [Locale.unfold_attrib])])]
||> Sign.restore_naming thy';
@@ -689,8 +688,7 @@
|> def_pred pname parms defs' (ints @ the_list a_pred) (ints' @ the_list a_pred);
val (_, thy'''') =
thy'''
- |> Sign.add_path (Binding.name_of pname)
- |> Sign.no_base_names
+ |> Sign.mandatory_path (Binding.name_of pname)
|> PureThy.note_thmss Thm.internalK
[((Binding.name introN, []), [([intro], [Locale.intro_attrib])]),
((Binding.name axiomsN, []),
--- a/src/Pure/Isar/local_theory.ML Thu Mar 12 15:31:26 2009 +0100
+++ b/src/Pure/Isar/local_theory.ML Thu Mar 12 15:31:44 2009 +0100
@@ -138,12 +138,12 @@
fun full_naming lthy =
Sign.naming_of (ProofContext.theory_of lthy)
- |> NameSpace.sticky_prefix (#theory_prefix (get_lthy lthy));
+ |> NameSpace.mandatory_path (#theory_prefix (get_lthy lthy));
fun full_name naming = NameSpace.full_name (full_naming naming);
fun theory_result f lthy = lthy |> raw_theory_result (fn thy => thy
- |> Sign.sticky_prefix (#theory_prefix (get_lthy lthy))
+ |> Sign.mandatory_path (#theory_prefix (get_lthy lthy))
|> f
||> Sign.restore_naming thy);
--- a/src/Pure/Isar/locale.ML Thu Mar 12 15:31:26 2009 +0100
+++ b/src/Pure/Isar/locale.ML Thu Mar 12 15:31:44 2009 +0100
@@ -161,7 +161,7 @@
| NONE => error ("Unknown locale " ^ quote name);
fun register_locale binding parameters spec intros axioms decls notes dependencies thy =
- thy |> LocalesData.map (NameSpace.bind (Sign.naming_of thy) (binding,
+ thy |> LocalesData.map (NameSpace.define (Sign.naming_of thy) (binding,
mk_locale ((parameters, spec, intros, axioms), ((decls, notes), dependencies))) #> snd);
fun change_locale name =
--- a/src/Pure/Isar/method.ML Thu Mar 12 15:31:26 2009 +0100
+++ b/src/Pure/Isar/method.ML Thu Mar 12 15:31:44 2009 +0100
@@ -394,7 +394,7 @@
val new_meths = raw_meths |> map (fn (name, f, comment) =>
(Binding.name name, ((f, comment), stamp ())));
- fun add meths = fold (snd oo NameSpace.bind (Sign.naming_of thy)) new_meths meths
+ fun add meths = fold (snd oo NameSpace.define (Sign.naming_of thy)) new_meths meths
handle Symtab.DUP dup => error ("Duplicate declaration of method " ^ quote dup);
in Methods.map add thy end;
--- a/src/Pure/Isar/proof_context.ML Thu Mar 12 15:31:26 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML Thu Mar 12 15:31:44 2009 +0100
@@ -97,7 +97,7 @@
val get_thms: Proof.context -> xstring -> thm list
val get_thm: Proof.context -> xstring -> thm
val add_path: string -> Proof.context -> Proof.context
- val sticky_prefix: string -> Proof.context -> Proof.context
+ val mandatory_path: string -> Proof.context -> Proof.context
val restore_naming: Proof.context -> Proof.context -> Proof.context
val reset_naming: Proof.context -> Proof.context
val note_thmss: string -> (Thm.binding * (Facts.ref * attribute list) list) list ->
@@ -945,7 +945,7 @@
(* name space operations *)
val add_path = map_naming o NameSpace.add_path;
-val sticky_prefix = map_naming o NameSpace.sticky_prefix;
+val mandatory_path = map_naming o NameSpace.mandatory_path;
val restore_naming = map_naming o K o naming_of;
val reset_naming = map_naming (K local_naming);
--- a/src/Pure/axclass.ML Thu Mar 12 15:31:26 2009 +0100
+++ b/src/Pure/axclass.ML Thu Mar 12 15:31:44 2009 +0100
@@ -370,8 +370,7 @@
val T' = Type.strip_sorts T;
in
thy
- |> Sign.sticky_prefix name_inst
- |> Sign.no_base_names
+ |> Sign.mandatory_path name_inst
|> Sign.declare_const [] ((Binding.name c', T'), NoSyn)
|-> (fn const' as Const (c'', _) =>
Thm.add_def false true
@@ -481,8 +480,7 @@
val class_triv = Thm.class_triv def_thy class;
val ([(_, [intro]), (_, classrel), (_, axioms)], facts_thy) =
def_thy
- |> Sign.add_path (Binding.name_of bconst)
- |> Sign.no_base_names
+ |> Sign.mandatory_path (Binding.name_of bconst)
|> PureThy.note_thmss ""
[((Binding.name introN, []), [([Drule.standard raw_intro], [])]),
((Binding.name superN, []), [(map Drule.standard raw_classrel, [])]),
--- a/src/Pure/consts.ML Thu Mar 12 15:31:26 2009 +0100
+++ b/src/Pure/consts.ML Thu Mar 12 15:31:44 2009 +0100
@@ -215,7 +215,7 @@
fun err_dup_const c =
error ("Duplicate declaration of constant " ^ quote c);
-fun extend_decls naming decl tab = NameSpace.bind naming decl tab
+fun extend_decls naming decl tab = NameSpace.define naming decl tab
handle Symtab.DUP c => err_dup_const c;
--- a/src/Pure/sign.ML Thu Mar 12 15:31:26 2009 +0100
+++ b/src/Pure/sign.ML Thu Mar 12 15:31:44 2009 +0100
@@ -124,7 +124,7 @@
val add_path: string -> theory -> theory
val root_path: theory -> theory
val parent_path: theory -> theory
- val sticky_prefix: string -> theory -> theory
+ val mandatory_path: string -> theory -> theory
val no_base_names: theory -> theory
val local_path: theory -> theory
val restore_naming: theory -> theory -> theory
@@ -619,7 +619,7 @@
val add_path = map_naming o NameSpace.add_path;
val root_path = map_naming NameSpace.root_path;
val parent_path = map_naming NameSpace.parent_path;
-val sticky_prefix = map_naming o NameSpace.sticky_prefix;
+val mandatory_path = map_naming o NameSpace.mandatory_path;
val no_base_names = map_naming NameSpace.no_base_names;
fun local_path thy = thy |> root_path |> add_path (Context.theory_name thy);
--- a/src/Pure/simplifier.ML Thu Mar 12 15:31:26 2009 +0100
+++ b/src/Pure/simplifier.ML Thu Mar 12 15:31:44 2009 +0100
@@ -222,7 +222,7 @@
val simproc' = morph_simproc phi simproc;
in
Simprocs.map (fn simprocs =>
- NameSpace.bind naming (b', simproc') simprocs |> snd
+ NameSpace.define naming (b', simproc') simprocs |> snd
handle Symtab.DUP dup => err_dup_simproc dup)
#> map_ss (fn ss => ss addsimprocs [simproc'])
end)
--- a/src/Pure/theory.ML Thu Mar 12 15:31:26 2009 +0100
+++ b/src/Pure/theory.ML Thu Mar 12 15:31:44 2009 +0100
@@ -175,7 +175,7 @@
fun gen_add_axioms prep_axm raw_axms thy = thy |> map_axioms (fn axioms =>
let
val axms = map (apsnd Logic.varify o prep_axm thy) raw_axms;
- val axioms' = fold (snd oo NameSpace.bind (Sign.naming_of thy)) axms axioms
+ val axioms' = fold (snd oo NameSpace.define (Sign.naming_of thy)) axms axioms
handle Symtab.DUP dup => err_dup_axm dup;
in axioms' end);
--- a/src/Pure/thm.ML Thu Mar 12 15:31:26 2009 +0100
+++ b/src/Pure/thm.ML Thu Mar 12 15:31:44 2009 +0100
@@ -1700,7 +1700,7 @@
fun add_oracle (b, oracle) thy =
let
val naming = Sign.naming_of thy;
- val (name, tab') = NameSpace.bind naming (b, serial ()) (Oracles.get thy)
+ val (name, tab') = NameSpace.define naming (b, serial ()) (Oracles.get thy)
handle Symtab.DUP _ => err_dup_ora (Binding.str_of b);
val thy' = Oracles.put tab' thy;
in ((name, invoke_oracle (Theory.check_thy thy') name oracle), thy') end;