Mercurial Mercurial > repos > isabelle / changelog
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | gz | help
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Mon, 09 Mar 2009 17:55:03 +0100 adapted to simplified ThyOutput.antiquotation interface;
changeset
wenzelm [Mon, 09 Mar 2009 17:55:03 +0100] rev 30392
adapted to simplified ThyOutput.antiquotation interface; fixed theory name;
Mon, 09 Mar 2009 17:54:27 +0100 adapted to simplified ThyOutput.antiquotation interface;
changeset
wenzelm [Mon, 09 Mar 2009 17:54:27 +0100] rev 30391
adapted to simplified ThyOutput.antiquotation interface;
Mon, 09 Mar 2009 17:53:53 +0100 simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output;
changeset
wenzelm [Mon, 09 Mar 2009 17:53:53 +0100] rev 30390
simplified interface to define document antiquotations, cf. antiquotatation, maybe_pretty_source, output; removed incomprehensible args parser setup; removed obsolete locale flag -- text is already localized; misc tuning and cleanup of concrete antiquotations; goal state antiquotations: ignore source flag;
Mon, 09 Mar 2009 15:49:55 +0100 merged
changeset
wenzelm [Mon, 09 Mar 2009 15:49:55 +0100] rev 30389
merged
Mon, 09 Mar 2009 14:44:04 +0100 merged
changeset
haftmann [Mon, 09 Mar 2009 14:44:04 +0100] rev 30388
merged
Mon, 09 Mar 2009 14:43:51 +0100 NameSpace.base_name ~> Long_Name.base_name
changeset
haftmann [Mon, 09 Mar 2009 14:43:51 +0100] rev 30387
NameSpace.base_name ~> Long_Name.base_name
Mon, 09 Mar 2009 14:20:07 +0100 Docs
changeset
nipkow [Mon, 09 Mar 2009 14:20:07 +0100] rev 30386
Docs
Mon, 09 Mar 2009 12:24:19 +0100 merged
changeset
nipkow [Mon, 09 Mar 2009 12:24:19 +0100] rev 30385
merged
Mon, 09 Mar 2009 12:24:01 +0100 fixed typing of UN/INT syntax
changeset
nipkow [Mon, 09 Mar 2009 12:24:01 +0100] rev 30384
fixed typing of UN/INT syntax
Mon, 09 Mar 2009 15:36:31 +0100 more contributors;
changeset
wenzelm [Mon, 09 Mar 2009 15:36:31 +0100] rev 30383
more contributors;
Mon, 09 Mar 2009 11:57:48 +0100 adapted ThyOutput.antiquotation;
changeset
wenzelm [Mon, 09 Mar 2009 11:57:48 +0100] rev 30382
adapted ThyOutput.antiquotation;
Mon, 09 Mar 2009 11:56:34 +0100 refined antiquotation interface: formally pass result context and (potential) result source;
changeset
wenzelm [Mon, 09 Mar 2009 11:56:34 +0100] rev 30381
refined antiquotation interface: formally pass result context and (potential) result source; removed redundant raw_antiquotation;
Mon, 09 Mar 2009 10:10:34 +0100 merged
changeset
haftmann [Mon, 09 Mar 2009 10:10:34 +0100] rev 30380
merged
Mon, 09 Mar 2009 09:37:33 +0100 binding replaces bstring
changeset
haftmann [Mon, 09 Mar 2009 09:37:33 +0100] rev 30379
binding replaces bstring
Mon, 09 Mar 2009 09:34:39 +0100 dropped eq_pred
changeset
haftmann [Mon, 09 Mar 2009 09:34:39 +0100] rev 30378
dropped eq_pred
Sun, 08 Mar 2009 17:25:16 +0100 merged
changeset
haftmann [Sun, 08 Mar 2009 17:25:16 +0100] rev 30377
merged
Sun, 08 Mar 2009 15:25:29 +0100 refined enumeration implementation
changeset
haftmann [Sun, 08 Mar 2009 15:25:29 +0100] rev 30376
refined enumeration implementation
Sun, 08 Mar 2009 15:25:29 +0100 added top and bot syntax
changeset
haftmann [Sun, 08 Mar 2009 15:25:29 +0100] rev 30375
added top and bot syntax
Sun, 08 Mar 2009 15:25:28 +0100 added predicate compiler, as formally checked prototype, not as user package
changeset
haftmann [Sun, 08 Mar 2009 15:25:28 +0100] rev 30374
added predicate compiler, as formally checked prototype, not as user package
Mon, 09 Mar 2009 10:01:58 +0100 attempt to bypass spurious infix syntax problem on polyml/sun
changeset
haftmann [Mon, 09 Mar 2009 10:01:58 +0100] rev 30373
attempt to bypass spurious infix syntax problem on polyml/sun
Mon, 09 Mar 2009 09:38:36 +0100 UN syntax fix
changeset
nipkow [Mon, 09 Mar 2009 09:38:36 +0100] rev 30372
UN syntax fix
Mon, 09 Mar 2009 09:24:50 +0100 merged
changeset
nipkow [Mon, 09 Mar 2009 09:24:50 +0100] rev 30371
merged
Mon, 09 Mar 2009 09:24:31 +0100 Docs updates
changeset
nipkow [Mon, 09 Mar 2009 09:24:31 +0100] rev 30370
Docs updates
Sun, 08 Mar 2009 21:35:39 +0100 use simplified ThyOutput.antiquotation;
changeset
wenzelm [Sun, 08 Mar 2009 21:35:39 +0100] rev 30369
use simplified ThyOutput.antiquotation; eliminated obscure structure alias;
Sun, 08 Mar 2009 21:12:37 +0100 added (raw_)antiquotation -- simplified wrapper for defining output commands;
changeset
wenzelm [Sun, 08 Mar 2009 21:12:37 +0100] rev 30368
added (raw_)antiquotation -- simplified wrapper for defining output commands;
Sun, 08 Mar 2009 20:31:54 +0100 simplified presentation: pass state directly;
changeset
wenzelm [Sun, 08 Mar 2009 20:31:54 +0100] rev 30367
simplified presentation: pass state directly;
Sun, 08 Mar 2009 20:31:01 +0100 simplified presentation: built into transaction, pass state directly;
changeset
wenzelm [Sun, 08 Mar 2009 20:31:01 +0100] rev 30366
simplified presentation: built into transaction, pass state directly;
Sun, 08 Mar 2009 17:37:18 +0100 adapted to structure Long_Name;
changeset
wenzelm [Sun, 08 Mar 2009 17:37:18 +0100] rev 30365
adapted to structure Long_Name;
Sun, 08 Mar 2009 17:26:14 +0100 moved basic algebra of long names from structure NameSpace to Long_Name;
changeset
wenzelm [Sun, 08 Mar 2009 17:26:14 +0100] rev 30364
moved basic algebra of long names from structure NameSpace to Long_Name;
Sun, 08 Mar 2009 17:19:15 +0100 proper local context for text with antiquotations;
changeset
wenzelm [Sun, 08 Mar 2009 17:19:15 +0100] rev 30363
proper local context for text with antiquotations;
Sun, 08 Mar 2009 17:05:43 +0100 more explicit warning message;
changeset
wenzelm [Sun, 08 Mar 2009 17:05:43 +0100] rev 30362
more explicit warning message;
Sun, 08 Mar 2009 17:03:07 +0100 added qualified_name -- emulates old-style qualified bstring;
changeset
wenzelm [Sun, 08 Mar 2009 17:03:07 +0100] rev 30361
added qualified_name -- emulates old-style qualified bstring; tuned;
Sun, 08 Mar 2009 16:53:38 +0100 added General/long_name.ML;
changeset
wenzelm [Sun, 08 Mar 2009 16:53:38 +0100] rev 30360
added General/long_name.ML;
Sun, 08 Mar 2009 16:53:07 +0100 moved basic algebra of long names from structure NameSpace to Long_Name;
changeset
wenzelm [Sun, 08 Mar 2009 16:53:07 +0100] rev 30359
moved basic algebra of long names from structure NameSpace to Long_Name; tuned signature;
Sun, 08 Mar 2009 15:01:10 +0100 index_ML: removed spurious writeln introduced in 41ce4f5c97c9 -- it merely produces unreadable LaTeX sources;
changeset
wenzelm [Sun, 08 Mar 2009 15:01:10 +0100] rev 30358
index_ML: removed spurious writeln introduced in 41ce4f5c97c9 -- it merely produces unreadable LaTeX sources;
Sun, 08 Mar 2009 12:16:12 +0100 proper context for Simplifier.pretty_ss;
changeset
wenzelm [Sun, 08 Mar 2009 12:16:12 +0100] rev 30357
proper context for Simplifier.pretty_ss;
Sun, 08 Mar 2009 12:15:58 +0100 added dest_ss;
changeset
wenzelm [Sun, 08 Mar 2009 12:15:58 +0100] rev 30356
added dest_ss; proper context fo pretty_ss; tuned;
Sun, 08 Mar 2009 00:41:52 +0100 use binding type;
changeset
wenzelm [Sun, 08 Mar 2009 00:41:52 +0100] rev 30355
use binding type;
Sun, 08 Mar 2009 00:16:34 +0100 merged
changeset
wenzelm [Sun, 08 Mar 2009 00:16:34 +0100] rev 30354
merged
Sat, 07 Mar 2009 23:41:04 +0100 merged
changeset
haftmann [Sat, 07 Mar 2009 23:41:04 +0100] rev 30353
merged
Sat, 07 Mar 2009 15:20:32 +0100 restructured theory Set.thy
changeset
haftmann [Sat, 07 Mar 2009 15:20:32 +0100] rev 30352
restructured theory Set.thy
Sat, 07 Mar 2009 23:37:09 +0100 merged
changeset
wenzelm [Sat, 07 Mar 2009 23:37:09 +0100] rev 30351
merged
Sat, 07 Mar 2009 17:05:40 +0100 Removed "nitpick_maybe" constant. Makarius now taught me a much nicer trick.
changeset
blanchet [Sat, 07 Mar 2009 17:05:40 +0100] rev 30350
Removed "nitpick_maybe" constant. Makarius now taught me a much nicer trick.
Sat, 07 Mar 2009 16:47:36 +0100 Added a second timeout mechanism to Refute.
changeset
blanchet [Sat, 07 Mar 2009 16:47:36 +0100] rev 30349
Added a second timeout mechanism to Refute. For some reason, TimeLimit.timeLimit often does not work, and it leaves Refute running forever, making any evaluation using Mutabelle or Mirabelle impossible. The redundant timeout seems to do the trick.
Sat, 07 Mar 2009 12:27:26 +0100 merged
changeset
blanchet [Sat, 07 Mar 2009 12:27:26 +0100] rev 30348
merged
Sat, 07 Mar 2009 12:26:56 +0100 Refute: Distinguish between "genuine" and "potential" in the newly added "expect" option.
changeset
blanchet [Sat, 07 Mar 2009 12:26:56 +0100] rev 30347
Refute: Distinguish between "genuine" and "potential" in the newly added "expect" option.
Sat, 07 Mar 2009 23:30:58 +0100 minimal adaptions for abstract binding type;
changeset
wenzelm [Sat, 07 Mar 2009 23:30:58 +0100] rev 30346
minimal adaptions for abstract binding type;
Sat, 07 Mar 2009 22:17:25 +0100 more uniform handling of binding in packages;
changeset
wenzelm [Sat, 07 Mar 2009 22:17:25 +0100] rev 30345
more uniform handling of binding in packages;
Sat, 07 Mar 2009 22:16:50 +0100 more uniform handling of binding in targets and derived elements;
changeset
wenzelm [Sat, 07 Mar 2009 22:16:50 +0100] rev 30344
more uniform handling of binding in targets and derived elements;
Sat, 07 Mar 2009 22:12:07 +0100 replace old bstring by binding for logical primitives: class, type, const etc.;
changeset
wenzelm [Sat, 07 Mar 2009 22:12:07 +0100] rev 30343
replace old bstring by binding for logical primitives: class, type, const etc.;
Sat, 07 Mar 2009 22:04:59 +0100 moved Thm.def_name(_optional) to more_thm.ML;
changeset
wenzelm [Sat, 07 Mar 2009 22:04:59 +0100] rev 30342
moved Thm.def_name(_optional) to more_thm.ML; moved old-style Thm.get_def to Drule.get_def;
Sat, 07 Mar 2009 21:57:36 +0100 adapted Syntax.const_name;
changeset
wenzelm [Sat, 07 Mar 2009 21:57:36 +0100] rev 30341
adapted Syntax.const_name;
Sat, 07 Mar 2009 21:20:17 +0100 canonical argument order for type_name, const_name;
changeset
wenzelm [Sat, 07 Mar 2009 21:20:17 +0100] rev 30340
canonical argument order for type_name, const_name;
Sat, 07 Mar 2009 21:19:24 +0100 added const_binding;
changeset
wenzelm [Sat, 07 Mar 2009 21:19:24 +0100] rev 30339
added const_binding;
Sat, 07 Mar 2009 21:18:37 +0100 added prefix_name, suffix_name;
changeset
wenzelm [Sat, 07 Mar 2009 21:18:37 +0100] rev 30338
added prefix_name, suffix_name; added eq_name; added opaque signature constraint to prevent accidental equality test;
Sat, 07 Mar 2009 12:07:30 +0100 Theory.add_axioms/add_defs: replaced old bstring by binding;
changeset
wenzelm [Sat, 07 Mar 2009 12:07:30 +0100] rev 30337
Theory.add_axioms/add_defs: replaced old bstring by binding;
Sat, 07 Mar 2009 11:45:56 +0100 renamed rep_ss to MetaSimplifier.internal_ss;
changeset
wenzelm [Sat, 07 Mar 2009 11:45:56 +0100] rev 30336
renamed rep_ss to MetaSimplifier.internal_ss;
Sat, 07 Mar 2009 11:32:31 +0100 Binding.str_of: removed verbose feature, include qualifier in output;
changeset
wenzelm [Sat, 07 Mar 2009 11:32:31 +0100] rev 30335
Binding.str_of: removed verbose feature, include qualifier in output; renamed Binding.add_prefix to Binding.prefix;
Sat, 07 Mar 2009 11:31:41 +0100 oracle: proper name position, tuned;
changeset
wenzelm [Sat, 07 Mar 2009 11:31:41 +0100] rev 30334
oracle: proper name position, tuned;
Sat, 07 Mar 2009 10:06:58 +0100 merged
changeset
haftmann [Sat, 07 Mar 2009 10:06:58 +0100] rev 30333
merged
(0) -30000 -10000 -3000 -1000 -300 -100 -60 +60 +100 +300 +1000 +3000 +10000 +30000 tip
isabelle