Mercurial Mercurial > repos > isabelle / file revisions
summary | shortlog | changelog | graph | tags | bookmarks | branches | file | revisions | annotate | diff | comparison | rss | help
(0) tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Pure/Isar/expression.ML
Mon, 05 Jan 2009 15:55:04 +0100 haftmann locale -> old_locale, new_locale -> locale file | diff | annotate
Mon, 05 Jan 2009 15:36:24 +0100 haftmann rearranged target theories file | diff | annotate
Thu, 01 Jan 2009 14:23:39 +0100 wenzelm avoid polymorphic equality; file | diff | annotate
Wed, 31 Dec 2008 18:53:17 +0100 wenzelm use regular Term.add_XXX etc.; file | diff | annotate
Tue, 30 Dec 2008 19:07:42 +0100 wenzelm prep_result: Thm.close_derivation of witness theorem avoids performance issues with proof terms; file | diff | annotate
Tue, 23 Dec 2008 14:29:27 +0100 ballarin More liberal consistency check for defines elements. file | diff | annotate
Fri, 19 Dec 2008 15:05:37 +0100 ballarin Merged. file | diff | annotate
Thu, 18 Dec 2008 11:16:48 +0100 Norbert Schirmer adapted statespace module to new locales; file | diff | annotate
Fri, 19 Dec 2008 14:31:07 +0100 ballarin Intro_locales_tac knows about defines elements; more robust export morphism. file | diff | annotate
Thu, 18 Dec 2008 20:19:49 +0100 ballarin Merged. file | diff | annotate
Wed, 17 Dec 2008 17:53:41 +0100 ballarin Prevent defines from being checked in interpretation. file | diff | annotate
Thu, 18 Dec 2008 19:52:11 +0100 ballarin Refactored: evaluate specification text only in locale declarations. file | diff | annotate
Tue, 16 Dec 2008 15:08:08 +0100 ballarin Finer-grained activation so that facts from earlier elements are available. file | diff | annotate
Tue, 16 Dec 2008 12:08:10 +0100 ballarin Use correct mode when parsing elements and conclusion. file | diff | annotate
Sun, 14 Dec 2008 15:43:04 +0100 ballarin Strict prefixes in locales expressions. file | diff | annotate
Fri, 12 Dec 2008 12:31:00 +0100 ballarin Equations in interpretation as goals. file | diff | annotate
Thu, 11 Dec 2008 17:56:34 +0100 ballarin Interpretation in theories: first version with equations. file | diff | annotate
Wed, 10 Dec 2008 17:19:25 +0100 ballarin Use prefix component of bindings for locale prefixes. file | diff | annotate
Wed, 10 Dec 2008 16:30:33 +0100 ballarin Preserve idents (expression in sublocale). file | diff | annotate
Wed, 10 Dec 2008 14:21:42 +0100 ballarin Satisfy a_axioms. file | diff | annotate
Wed, 10 Dec 2008 10:12:44 +0100 ballarin Merged. file | diff | annotate
Wed, 10 Dec 2008 10:11:18 +0100 ballarin Enable keyword 'structure' in for clause of locale expression. file | diff | annotate
Tue, 09 Dec 2008 22:00:39 +0100 ballarin Correct order of defines in specification. file | diff | annotate
Tue, 09 Dec 2008 21:27:00 +0100 ballarin Pass on defines in inheritance; reject illicit defines created by instantiation. file | diff | annotate
Tue, 09 Dec 2008 15:34:49 +0100 ballarin Order of implicit parameters in locale expression. file | diff | annotate
Tue, 09 Dec 2008 11:30:24 +0100 ballarin When adding locales, delay notes until local theory is built. file | diff | annotate
Mon, 08 Dec 2008 21:33:50 +0100 ballarin Default names for definitions. file | diff | annotate
Mon, 08 Dec 2008 18:44:24 +0100 ballarin Proper shape of assumptions generated from Defines elements. file | diff | annotate
Mon, 08 Dec 2008 14:22:42 +0100 ballarin Merged. file | diff | annotate
Mon, 08 Dec 2008 14:18:29 +0100 ballarin Explicitly close up defines. file | diff | annotate
Fri, 05 Dec 2008 16:41:36 +0100 ballarin Interpretation in proof contexts. file | diff | annotate
Fri, 05 Dec 2008 18:43:42 +0100 haftmann Name.name_of -> Binding.base_name file | diff | annotate
Fri, 05 Dec 2008 11:42:27 +0100 ballarin Merged. file | diff | annotate
Fri, 05 Dec 2008 11:26:07 +0100 ballarin Interpretation in theories including interaction with subclass relation. file | diff | annotate
Fri, 05 Dec 2008 08:04:53 +0100 haftmann dropped NameSpace.declare_base file | diff | annotate
Thu, 04 Dec 2008 14:43:33 +0100 haftmann cleaned up binding module and related code file | diff | annotate
Wed, 03 Dec 2008 15:27:41 +0100 ballarin Sublocale: removed public after_qed; identifiers private to NewLocale. file | diff | annotate
Mon, 01 Dec 2008 16:59:31 +0100 ballarin No resolution of patterns within context statements. file | diff | annotate
Fri, 28 Nov 2008 17:43:06 +0100 ballarin Intro_locales_tac to simplify goals involving locale predicates. file | diff | annotate
Fri, 28 Nov 2008 12:26:14 +0100 ballarin Ahere to modern naming conventions; proper treatment of internal vs external names. file | diff | annotate
Thu, 27 Nov 2008 21:25:34 +0100 ballarin Proper treatment of expressions with free arguments. file | diff | annotate
Thu, 27 Nov 2008 10:29:07 +0100 ballarin Sublocale command. file | diff | annotate
Tue, 25 Nov 2008 18:06:21 +0100 ballarin Expression types cleaned up, proper treatment of term patterns. file | diff | annotate
Mon, 24 Nov 2008 18:03:48 +0100 ballarin Read/cert_statement for theorem statements. file | diff | annotate
Fri, 21 Nov 2008 18:01:39 +0100 ballarin add_locale functional. file | diff | annotate
Thu, 20 Nov 2008 14:55:28 +0100 haftmann tuned name bindings file | diff | annotate
Thu, 20 Nov 2008 10:29:35 +0100 ballarin Deleted debug message (PolyML). file | diff | annotate
Wed, 19 Nov 2008 17:04:29 +0100 ballarin Type inference for elements through syntax module. file | diff | annotate
Tue, 18 Nov 2008 09:40:06 +0100 ballarin Activate elements moved to element.ML. file | diff | annotate
Fri, 14 Nov 2008 16:49:52 +0100 ballarin Initial part of locale reimplementation. file | diff | annotate
Tue, 28 Oct 2008 12:28:14 +0100 haftmann making SMLNJ happy file | diff | annotate
Mon, 27 Oct 2008 16:23:54 +0100 ballarin New-style locale expressions with instantiation (new file expression.ML). file | diff | annotate
less more (0) tip
isabelle