| Wed, 23 Jan 2019 17:54:50 +0000 |
haftmann |
combinator to lift local theory update to theory update
|
file |
diff |
annotate
|
| Thu, 24 Sep 2015 23:33:29 +0200 |
wenzelm |
more explicit Defs.context: use proper name spaces as far as possible;
|
file |
diff |
annotate
|
| Wed, 23 Sep 2015 09:50:38 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 22 Sep 2015 22:38:22 +0200 |
wenzelm |
eliminated separate type Theory.dep: use typeargs uniformly for consts/types;
|
file |
diff |
annotate
|
| Tue, 22 Sep 2015 17:15:55 +0200 |
wenzelm |
clarified deps entry: global names for arguments;
|
file |
diff |
annotate
|
| Tue, 22 Sep 2015 15:58:19 +0200 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Tue, 22 Sep 2015 14:32:23 +0200 |
wenzelm |
HOL typedef with explicit dependency checks according to Ondrey Kuncar, 07-Jul-2015, 16-Jul-2015, 30-Jul-2015;
|
file |
diff |
annotate
|
| Wed, 08 Apr 2015 19:39:08 +0200 |
wenzelm |
proper context for Object_Logic operations;
|
file |
diff |
annotate
|
| Mon, 12 May 2014 17:17:32 +0200 |
wenzelm |
tuned signature to make axiomatizations more easy to spot in the source, via "add_axioms" or "axiomatization";
|
file |
diff |
annotate
|
| Wed, 26 Mar 2014 14:41:52 +0100 |
wenzelm |
prefer Context_Position where a context is available;
|
file |
diff |
annotate
|
| Wed, 10 Apr 2013 15:30:19 +0200 |
wenzelm |
more standard module name Axclass (according to file name);
|
file |
diff |
annotate
|
| Sun, 18 Mar 2012 13:04:22 +0100 |
wenzelm |
maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming);
|
file |
diff |
annotate
|
| Sun, 17 Apr 2011 21:42:47 +0200 |
wenzelm |
added Binding.print convenience, which includes quote already;
|
file |
diff |
annotate
|
| Sun, 17 Apr 2011 19:54:04 +0200 |
wenzelm |
report Name_Space.declare/define, relatively to context;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 15:47:52 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Fri, 27 Aug 2010 19:43:28 +0200 |
wenzelm |
more careful treatment of context visibility flag wrt. spurious warnings;
|
file |
diff |
annotate
|
| Thu, 26 Aug 2010 15:48:08 +0200 |
wenzelm |
renamed Local_Theory.theory(_result) to Local_Theory.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
|
file |
diff |
annotate
|
| Thu, 12 Aug 2010 13:23:46 +0200 |
haftmann |
Named_Target.theory_init
|
file |
diff |
annotate
|
| Wed, 11 Aug 2010 14:45:38 +0200 |
haftmann |
renamed Theory_Target to the more appropriate Named_Target
|
file |
diff |
annotate
|
| Wed, 28 Apr 2010 16:11:13 +0200 |
wenzelm |
tuned user-level type abbrevs: explicit warning concerning ignored sort constraints -- sorts never affect formation of types and type abbrevs strip sorts internally;
|
file |
diff |
annotate
|
| Fri, 16 Apr 2010 22:45:07 +0200 |
wenzelm |
replaced old Sign.add_tyabbrs(_i) by Sign.add_type_abbrev (without mixfix);
|
file |
diff |
annotate
|
| Fri, 16 Apr 2010 20:56:40 +0200 |
wenzelm |
allow syntax types within abbreviations;
|
file |
diff |
annotate
|
| Fri, 16 Apr 2010 19:43:06 +0200 |
wenzelm |
local type abbreviations;
|
file |
diff |
annotate
|
| Thu, 15 Apr 2010 20:31:21 +0200 |
wenzelm |
explicit ProofContext.check_tfree;
|
file |
diff |
annotate
|
| Thu, 15 Apr 2010 18:09:22 +0200 |
wenzelm |
replaced slightly odd Typedecl.predeclare_constraints by plain declaration of type arguments -- also avoid "recursive" declaration of type constructor, which can cause problems with sequential definitions B.foo = A.foo;
|
file |
diff |
annotate
|
| Fri, 19 Mar 2010 00:41:34 +0100 |
wenzelm |
support type arguments with sort constraints;
|
file |
diff |
annotate
|
| Thu, 18 Mar 2010 22:56:32 +0100 |
wenzelm |
eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints (which also works for recursive types);
|
file |
diff |
annotate
|
| Sat, 13 Mar 2010 14:41:37 +0100 |
wenzelm |
added typedecl_wrt, which affects default sorts of type args;
|
file |
diff |
annotate
|
| Thu, 11 Mar 2010 18:52:50 +0100 |
wenzelm |
actually apply morphism to binding;
|
file |
diff |
annotate
|
| Tue, 09 Mar 2010 23:32:13 +0100 |
wenzelm |
localized typedecl;
|
file |
diff |
annotate
|
| Sun, 07 Mar 2010 12:47:02 +0100 |
wenzelm |
separate structure Typedecl;
|
file |
diff |
annotate
|