| Thu, 13 Nov 2008 14:19:10 +0100 |
haftmann |
proper name morphisms for locales
|
file |
diff |
annotate
|
| Mon, 10 Nov 2008 19:42:22 +0100 |
haftmann |
restruced naming code in anticipation of introduction of name morphisms
|
file |
diff |
annotate
|
| Mon, 10 Nov 2008 08:18:58 +0100 |
haftmann |
using explicit interpretaton prefix in Name.binding (still on the surface)
|
file |
diff |
annotate
|
| Thu, 30 Oct 2008 10:57:45 +0100 |
ballarin |
Dropped context element 'includes'.
|
file |
diff |
annotate
|
| Mon, 27 Oct 2008 16:14:51 +0100 |
ballarin |
Extension of interface: declarations_of.
|
file |
diff |
annotate
|
| Fri, 26 Sep 2008 19:07:56 +0200 |
wenzelm |
eliminated polymorphic equality;
|
file |
diff |
annotate
|
| Wed, 17 Sep 2008 15:21:30 +0200 |
ballarin |
Public interface to interpretation morphism.
|
file |
diff |
annotate
|
| Tue, 16 Sep 2008 12:27:05 +0200 |
ballarin |
Clearer separation of interpretation frontend and backend.
|
file |
diff |
annotate
|
| Wed, 03 Sep 2008 17:47:30 +0200 |
wenzelm |
Sign.declare_const: Name.binding;
|
file |
diff |
annotate
|
| Wed, 03 Sep 2008 11:44:48 +0200 |
wenzelm |
Name.qualified;
|
file |
diff |
annotate
|
| Tue, 02 Sep 2008 17:31:20 +0200 |
ballarin |
Interpretation commands no longer accept interpretation attributes.
|
file |
diff |
annotate
|
| Tue, 02 Sep 2008 16:55:33 +0200 |
wenzelm |
type Attrib.binding abbreviates Name.binding without attributes;
|
file |
diff |
annotate
|
| Tue, 02 Sep 2008 14:10:45 +0200 |
wenzelm |
explicit type Name.binding for higher-specification elements;
|
file |
diff |
annotate
|
| Thu, 28 Aug 2008 22:08:11 +0200 |
haftmann |
no parameter prefix for class interpretation
|
file |
diff |
annotate
|
| Wed, 27 Aug 2008 17:54:31 +0200 |
ballarin |
Consistent naming of theorems in interpretation.
|
file |
diff |
annotate
|
| Wed, 27 Aug 2008 12:00:28 +0200 |
wenzelm |
get rid of tabs;
|
file |
diff |
annotate
|
| Tue, 26 Aug 2008 16:04:22 +0200 |
ballarin |
Reorganisation of registration code.
|
file |
diff |
annotate
|
| Thu, 14 Aug 2008 16:52:46 +0200 |
wenzelm |
moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
|
file |
diff |
annotate
|
| Wed, 06 Aug 2008 16:41:40 +0200 |
ballarin |
Interpretation command (theory/proof context) no longer simplifies goal.
|
file |
diff |
annotate
|
| Fri, 01 Aug 2008 17:41:37 +0200 |
ballarin |
Removed import and lparams from locale record.
|
file |
diff |
annotate
|
| Wed, 30 Jul 2008 07:33:59 +0200 |
haftmann |
facts_of
|
file |
diff |
annotate
|
| Tue, 29 Jul 2008 08:15:44 +0200 |
haftmann |
tuned; explicit export of element accessors
|
file |
diff |
annotate
|
| Sat, 26 Jul 2008 09:00:26 +0200 |
haftmann |
tuned function name
|
file |
diff |
annotate
|
| Fri, 25 Jul 2008 12:03:32 +0200 |
haftmann |
dropped locale (open)
|
file |
diff |
annotate
|
| Sun, 18 May 2008 15:04:41 +0200 |
wenzelm |
Syntax.string_of_typ: proper context;
|
file |
diff |
annotate
|
| Mon, 14 Apr 2008 17:54:56 +0200 |
ballarin |
Changed naming scheme for theorems generated by interpretations.
|
file |
diff |
annotate
|
| Sat, 12 Apr 2008 17:00:48 +0200 |
wenzelm |
replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression);
|
file |
diff |
annotate
|
| Fri, 28 Mar 2008 20:02:04 +0100 |
wenzelm |
Context.>> : operate on Context.generic;
|
file |
diff |
annotate
|
| Thu, 27 Mar 2008 15:32:15 +0100 |
wenzelm |
eliminated delayed theory setup
|
file |
diff |
annotate
|
| Thu, 20 Mar 2008 00:20:49 +0100 |
wenzelm |
renamed former get_thms(_silent) to get_fact(_silent);
|
file |
diff |
annotate
|
| Mon, 17 Mar 2008 18:36:04 +0100 |
wenzelm |
closeup: recover original order of free variables!
|
file |
diff |
annotate
|
| Wed, 05 Mar 2008 22:58:11 +0100 |
wenzelm |
closeup: minor tuning of term traversal;
|
file |
diff |
annotate
|
| Mon, 17 Dec 2007 17:57:52 +0100 |
haftmann |
explicit closing of derived witnesses
|
file |
diff |
annotate
|
| Thu, 13 Dec 2007 07:09:07 +0100 |
haftmann |
memorizing and exporting destruction rules
|
file |
diff |
annotate
|
| Thu, 08 Nov 2007 22:19:43 +0100 |
wenzelm |
avoid "import" as identifier, which is a keyword in Alice;
|
file |
diff |
annotate
|
| Mon, 05 Nov 2007 17:48:51 +0100 |
ballarin |
Use of export rather than standard in interpretation.
|
file |
diff |
annotate
|
| Fri, 02 Nov 2007 18:53:01 +0100 |
haftmann |
generic tactic Method.intros_tac
|
file |
diff |
annotate
|
| Fri, 19 Oct 2007 12:22:12 +0200 |
ballarin |
Interpretation equations may have name and/or attribute;
|
file |
diff |
annotate
|
| Wed, 17 Oct 2007 23:16:34 +0200 |
wenzelm |
locale pred: authentic syntax, tuned aprop_tr' accordingly;
|
file |
diff |
annotate
|
| Wed, 17 Oct 2007 13:55:37 +0200 |
wenzelm |
clarified naming conventions of 'parse' and 'check' (as opposed to former 'cert');
|
file |
diff |
annotate
|
| Mon, 15 Oct 2007 15:29:43 +0200 |
haftmann |
canonical interpretation interface
|
file |
diff |
annotate
|
| Fri, 12 Oct 2007 14:42:30 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Wed, 10 Oct 2007 17:32:00 +0200 |
wenzelm |
removed redundant strip_vars/abs_eqn, use improved Drule.abs_def instead;
|
file |
diff |
annotate
|
| Wed, 10 Oct 2007 10:55:37 +0200 |
ballarin |
Prepare proper interface of interpretation_i, interpret_i.
|
file |
diff |
annotate
|
| Tue, 09 Oct 2007 00:20:13 +0200 |
wenzelm |
generic Syntax.pretty/string_of operations;
|
file |
diff |
annotate
|
| Mon, 01 Oct 2007 12:24:07 +0200 |
ballarin |
Theory/context data restructured; simplified interface for printing of interpretations.
|
file |
diff |
annotate
|
| Sat, 29 Sep 2007 08:58:56 +0200 |
haftmann |
exported intern_expr
|
file |
diff |
annotate
|
| Mon, 24 Sep 2007 21:07:38 +0200 |
wenzelm |
eliminated ProofContext.read_termTs;
|
file |
diff |
annotate
|
| Tue, 18 Sep 2007 18:50:17 +0200 |
ballarin |
Morphisms applied in global interpretations behave correctly on types and terms.
|
file |
diff |
annotate
|
| Tue, 04 Sep 2007 14:32:29 +0200 |
ballarin |
Improved comment.
|
file |
diff |
annotate
|
| Sat, 28 Jul 2007 20:40:24 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 27 Jul 2007 20:11:49 +0200 |
wenzelm |
Druke.dummy_thm;
|
file |
diff |
annotate
|
| Mon, 23 Jul 2007 13:47:48 +0200 |
ballarin |
interpretation: unfolding of equations;
|
file |
diff |
annotate
|
| Sun, 08 Jul 2007 19:51:58 +0200 |
wenzelm |
replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
|
file |
diff |
annotate
|
| Thu, 05 Jul 2007 20:01:28 +0200 |
wenzelm |
simplified ObjectLogic.atomize;
|
file |
diff |
annotate
|
| Tue, 19 Jun 2007 23:15:27 +0200 |
wenzelm |
balanced conjunctions;
|
file |
diff |
annotate
|
| Sun, 03 Jun 2007 23:16:56 +0200 |
wenzelm |
added gen_merge_lists/merge_lists/merge_alists (legacy operations from library.ML);
|
file |
diff |
annotate
|
| Thu, 31 May 2007 23:47:36 +0200 |
wenzelm |
simplified/unified list fold;
|
file |
diff |
annotate
|
| Mon, 07 May 2007 00:49:59 +0200 |
wenzelm |
simplified DataFun interfaces;
|
file |
diff |
annotate
|
| Thu, 26 Apr 2007 12:00:05 +0200 |
wenzelm |
renamed some old names Theory.xxx to Sign.xxx;
|
file |
diff |
annotate
|
| Mon, 23 Apr 2007 20:44:11 +0200 |
wenzelm |
read_instantiations: proper type-inference with fixed variables, infer parameter types as well;
|
file |
diff |
annotate
|
| Fri, 20 Apr 2007 16:54:57 +0200 |
ballarin |
Interpretation equations applied to attributes;
|
file |
diff |
annotate
|
| Sun, 15 Apr 2007 14:32:00 +0200 |
wenzelm |
Thm.fold_terms;
|
file |
diff |
annotate
|
| Sat, 14 Apr 2007 17:36:05 +0200 |
wenzelm |
Term.string_of_vname;
|
file |
diff |
annotate
|
| Fri, 13 Apr 2007 10:01:43 +0200 |
ballarin |
Experimental interpretation code for definitions.
|
file |
diff |
annotate
|
| Tue, 03 Apr 2007 19:24:19 +0200 |
wenzelm |
avoid clash with Alice keywords;
|
file |
diff |
annotate
|
| Mon, 26 Mar 2007 14:53:06 +0200 |
haftmann |
exported interface for intro rules
|
file |
diff |
annotate
|
| Fri, 23 Feb 2007 08:39:24 +0100 |
haftmann |
locale: add_locale accepts explicit predicate name, interpretation supports non-mandatory prefixes
|
file |
diff |
annotate
|
| Mon, 19 Feb 2007 16:44:08 +0100 |
schirmer |
more precise error message in parameter unification
|
file |
diff |
annotate
|
| Sat, 10 Feb 2007 09:26:19 +0100 |
haftmann |
internal interfaces for interpretation and interpret
|
file |
diff |
annotate
|
| Sun, 04 Feb 2007 22:02:21 +0100 |
wenzelm |
interpretation: attempt to be more serious about name_morphism;
|
file |
diff |
annotate
|
| Sat, 30 Dec 2006 16:08:00 +0100 |
wenzelm |
removed conditional combinator;
|
file |
diff |
annotate
|
| Thu, 07 Dec 2006 23:16:55 +0100 |
wenzelm |
reorganized structure Tactic vs. MetaSimplifier;
|
file |
diff |
annotate
|
| Thu, 07 Dec 2006 17:58:52 +0100 |
wenzelm |
tuned print_locale output;
|
file |
diff |
annotate
|
| Wed, 06 Dec 2006 21:19:03 +0100 |
wenzelm |
export: added explicit term operation;
|
file |
diff |
annotate
|
| Tue, 05 Dec 2006 22:14:50 +0100 |
wenzelm |
encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
|
file |
diff |
annotate
|
| Thu, 30 Nov 2006 14:17:25 +0100 |
wenzelm |
Goal.norm/close_result;
|
file |
diff |
annotate
|
| Wed, 29 Nov 2006 23:33:09 +0100 |
wenzelm |
*** bad commit -- reverted to previous version ***
|
file |
diff |
annotate
|
| Wed, 29 Nov 2006 23:28:11 +0100 |
wenzelm |
simplified add_thmss;
|
file |
diff |
annotate
|
| Wed, 29 Nov 2006 04:11:15 +0100 |
wenzelm |
simplified add_thmss;
|
file |
diff |
annotate
|
| Sun, 26 Nov 2006 18:07:25 +0100 |
wenzelm |
Element.map_ctxt_attrib;
|
file |
diff |
annotate
|
| Fri, 24 Nov 2006 22:05:19 +0100 |
wenzelm |
tuned morphisms;
|
file |
diff |
annotate
|
| Thu, 23 Nov 2006 20:33:39 +0100 |
wenzelm |
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
|
file |
diff |
annotate
|
| Thu, 23 Nov 2006 00:52:23 +0100 |
wenzelm |
replaced Args.map_values/Element.map_ctxt_values by general morphism application;
|
file |
diff |
annotate
|
| Tue, 21 Nov 2006 18:07:38 +0100 |
wenzelm |
notes: proper kind;
|
file |
diff |
annotate
|
| Wed, 15 Nov 2006 20:50:24 +0100 |
wenzelm |
add_locale: re-init result context (avoids subtle modifications after introducing predicate views internally);
|
file |
diff |
annotate
|
| Tue, 14 Nov 2006 22:17:01 +0100 |
wenzelm |
replaced Variable.fix_frees by Variable.auto_fixes (depends on body mode);
|
file |
diff |
annotate
|
| Tue, 14 Nov 2006 15:29:55 +0100 |
wenzelm |
simplified Proof.theorem(_i) interface;
|
file |
diff |
annotate
|
| Thu, 09 Nov 2006 11:58:50 +0100 |
wenzelm |
removed obsolete locale_results;
|
file |
diff |
annotate
|
| Tue, 07 Nov 2006 19:40:56 +0100 |
wenzelm |
removed obsolete theorem statements (cf. specification.ML);
|
file |
diff |
annotate
|
| Tue, 07 Nov 2006 18:14:53 +0100 |
schirmer |
exported intro_locales_tac
|
file |
diff |
annotate
|
| Sat, 14 Oct 2006 23:25:54 +0200 |
wenzelm |
export map_elem;
|
file |
diff |
annotate
|
| Thu, 12 Oct 2006 22:57:38 +0200 |
wenzelm |
interpretation_in_locale: standalone goal setup;
|
file |
diff |
annotate
|
| Wed, 11 Oct 2006 00:31:38 +0200 |
wenzelm |
add_locale(_i): return actual result context;
|
file |
diff |
annotate
|
| Tue, 10 Oct 2006 13:59:13 +0200 |
haftmann |
gen_rem(s) abandoned in favour of remove / subtract
|
file |
diff |
annotate
|
| Mon, 09 Oct 2006 02:20:04 +0200 |
wenzelm |
removed obsolete note_thmss(_i);
|
file |
diff |
annotate
|
| Sat, 07 Oct 2006 01:30:58 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 21 Sep 2006 19:04:20 +0200 |
wenzelm |
member (op =);
|
file |
diff |
annotate
|
| Fri, 15 Sep 2006 22:56:13 +0200 |
wenzelm |
renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
|
file |
diff |
annotate
|
| Wed, 09 Aug 2006 00:12:38 +0200 |
wenzelm |
global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
|
file |
diff |
annotate
|
| Thu, 03 Aug 2006 14:53:57 +0200 |
ballarin |
Updated comments.
|
file |
diff |
annotate
|
| Wed, 02 Aug 2006 22:27:01 +0200 |
wenzelm |
removed obsolete Drule.frees/vars_of etc.;
|
file |
diff |
annotate
|
| Thu, 27 Jul 2006 23:28:28 +0200 |
wenzelm |
renamed ProofContext.fix_frees to Variable.fix_frees;
|
file |
diff |
annotate
|
| Thu, 27 Jul 2006 13:43:01 +0200 |
wenzelm |
moved basic assumption operations from structure ProofContext to Assumption;
|
file |
diff |
annotate
|
| Tue, 25 Jul 2006 21:18:02 +0200 |
wenzelm |
renamed add_term_varnames to Term.add_varnames (cf. Term.add_vars etc.);
|
file |
diff |
annotate
|
| Wed, 19 Jul 2006 19:24:02 +0200 |
ballarin |
Strict dfs traversal of imported and registered identifiers.
|
file |
diff |
annotate
|
| Tue, 11 Jul 2006 12:24:23 +0200 |
wenzelm |
Name.internal;
|
file |
diff |
annotate
|
| Tue, 11 Jul 2006 11:19:28 +0200 |
ballarin |
Witness theorems of interpretations now transfered to current theory.
|
file |
diff |
annotate
|
| Sat, 08 Jul 2006 12:54:47 +0200 |
wenzelm |
Element.prove_witness: context;
|
file |
diff |
annotate
|
| Fri, 07 Jul 2006 09:39:25 +0200 |
ballarin |
Fixed erroneous check-in.
|
file |
diff |
annotate
|
| Fri, 07 Jul 2006 09:28:39 +0200 |
ballarin |
Internal restructuring: identify no longer computes syntax.
|
file |
diff |
annotate
|
| Thu, 06 Jul 2006 23:36:40 +0200 |
wenzelm |
removed obsolete locale view;
|
file |
diff |
annotate
|
| Tue, 04 Jul 2006 15:45:59 +0200 |
ballarin |
Locales no longer generate views. The following functions have changed
|
file |
diff |
annotate
|
| Tue, 04 Jul 2006 14:47:01 +0200 |
ballarin |
Method intro_locales replaced by intro_locales and unfold_locales.
|
file |
diff |
annotate
|
| Thu, 22 Jun 2006 07:08:04 +0200 |
ballarin |
Improved handling of defines imported in duplicate.
|
file |
diff |
annotate
|
| Tue, 20 Jun 2006 16:46:30 +0200 |
haftmann |
fixed sml/nj value restriction problem
|
file |
diff |
annotate
|
| Tue, 20 Jun 2006 15:53:44 +0200 |
ballarin |
Restructured locales with predicates: import is now an interpretation.
|
file |
diff |
annotate
|
| Sat, 17 Jun 2006 19:37:55 +0200 |
wenzelm |
Variable.importT_inst;
|
file |
diff |
annotate
|
| Thu, 15 Jun 2006 23:10:45 +0200 |
wenzelm |
ProofContext: moved variable operations to struct Variable;
|
file |
diff |
annotate
|
| Tue, 13 Jun 2006 23:41:31 +0200 |
wenzelm |
use Drule.unvarify instead of obsolete Drule.freeze_all;
|
file |
diff |
annotate
|
| Wed, 07 Jun 2006 02:01:33 +0200 |
wenzelm |
renamed Type.(un)varifyT to Logic.(un)varifyT;
|
file |
diff |
annotate
|
| Tue, 06 Jun 2006 10:05:57 +0200 |
ballarin |
Improved parameter management of locales.
|
file |
diff |
annotate
|
| Mon, 05 Jun 2006 21:54:26 +0200 |
wenzelm |
export read/cert_expr;
|
file |
diff |
annotate
|
| Fri, 26 May 2006 22:20:06 +0200 |
wenzelm |
activate Defines: fix frees;
|
file |
diff |
annotate
|
| Tue, 16 May 2006 21:33:16 +0200 |
wenzelm |
replaced abbrevs by term_syntax, which is both simpler and more general;
|
file |
diff |
annotate
|
| Sun, 07 May 2006 00:22:05 +0200 |
wenzelm |
removed 'concl is' patterns;
|
file |
diff |
annotate
|
| Thu, 27 Apr 2006 15:06:35 +0200 |
wenzelm |
tuned basic list operators (flat, maps, map_filter);
|
file |
diff |
annotate
|
| Thu, 13 Apr 2006 12:01:01 +0200 |
wenzelm |
use conjunction stuff from conjunction.ML;
|
file |
diff |
annotate
|
| Sat, 08 Apr 2006 22:51:26 +0200 |
wenzelm |
abbrevs: support print mode;
|
file |
diff |
annotate
|
| Mon, 20 Mar 2006 21:29:04 +0100 |
wenzelm |
interpret: Proof.assert_forward_or_chain;
|
file |
diff |
annotate
|
| Mon, 20 Mar 2006 17:15:35 +0100 |
ballarin |
Tuned signature of Locale.add_locale(_i).
|
file |
diff |
annotate
|
| Fri, 17 Mar 2006 15:22:40 +0100 |
ballarin |
add_locale(_i) returns internal locale name.
|
file |
diff |
annotate
|
| Fri, 17 Mar 2006 09:57:25 +0100 |
ballarin |
Internal restructuring: local parameters.
|
file |
diff |
annotate
|
| Thu, 16 Mar 2006 20:19:25 +0100 |
ballarin |
New interface function parameters_of_expr.
|
file |
diff |
annotate
|
| Wed, 15 Feb 2006 21:35:11 +0100 |
wenzelm |
removed distinct, renamed gen_distinct to distinct;
|
file |
diff |
annotate
|
| Sun, 12 Feb 2006 21:34:18 +0100 |
wenzelm |
simplified TableFun.join;
|
file |
diff |
annotate
|
| Sat, 11 Feb 2006 17:17:53 +0100 |
wenzelm |
added abbreviations: activated by init, no expressions yet;
|
file |
diff |
annotate
|
| Tue, 07 Feb 2006 19:56:45 +0100 |
wenzelm |
renamed gen_duplicates to duplicates;
|
file |
diff |
annotate
|
| Mon, 06 Feb 2006 20:59:52 +0100 |
wenzelm |
TableFun: renamed xxx_multi to xxx_list;
|
file |
diff |
annotate
|
| Fri, 03 Feb 2006 11:47:57 +0100 |
haftmann |
refined signature of locale module
|
file |
diff |
annotate
|
| Thu, 02 Feb 2006 16:31:35 +0100 |
wenzelm |
Proof.refine_insert;
|
file |
diff |
annotate
|
| Thu, 02 Feb 2006 12:54:08 +0100 |
wenzelm |
theorem(_in_locale): Element.statement, Obtain.statement;
|
file |
diff |
annotate
|
| Thu, 02 Feb 2006 10:12:45 +0100 |
ballarin |
*_asms_of fixed.
|
file |
diff |
annotate
|
| Sat, 28 Jan 2006 17:29:49 +0100 |
wenzelm |
LocalDefs;
|
file |
diff |
annotate
|
| Fri, 27 Jan 2006 19:03:12 +0100 |
wenzelm |
init: include view;
|
file |
diff |
annotate
|
| Fri, 27 Jan 2006 16:05:23 +0100 |
ballarin |
Interface to access the specification of a named locale.
|
file |
diff |
annotate
|
| Wed, 25 Jan 2006 00:21:40 +0100 |
wenzelm |
turned abstract_term into ProofContext.abs_def;
|
file |
diff |
annotate
|
| Tue, 24 Jan 2006 00:43:31 +0100 |
wenzelm |
removed the_params;
|
file |
diff |
annotate
|
| Sun, 22 Jan 2006 18:45:59 +0100 |
wenzelm |
added the_params;
|
file |
diff |
annotate
|
| Sat, 21 Jan 2006 23:02:14 +0100 |
wenzelm |
simplified type attribute;
|
file |
diff |
annotate
|
| Thu, 19 Jan 2006 21:22:08 +0100 |
wenzelm |
setup: theory -> theory;
|
file |
diff |
annotate
|
| Mon, 16 Jan 2006 21:55:15 +0100 |
wenzelm |
put_facts: do not pretend local thms were named;
|
file |
diff |
annotate
|
| Sat, 14 Jan 2006 17:14:06 +0100 |
wenzelm |
sane ERROR handling;
|
file |
diff |
annotate
|
| Fri, 13 Jan 2006 01:13:15 +0100 |
wenzelm |
uniform handling of fixes;
|
file |
diff |
annotate
|
| Sat, 07 Jan 2006 23:27:58 +0100 |
wenzelm |
added init;
|
file |
diff |
annotate
|
| Wed, 04 Jan 2006 10:28:31 +0100 |
haftmann |
fix: reintroduced pred_ctxt in gen_add_locale
|
file |
diff |
annotate
|
| Tue, 03 Jan 2006 11:32:16 +0100 |
haftmann |
add_local_context now yields imported and body elements seperatly; additional slight clenup in code
|
file |
diff |
annotate
|
| Tue, 03 Jan 2006 00:06:28 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 23 Dec 2005 15:16:53 +0100 |
wenzelm |
Logic.mk_conjunction_list;
|
file |
diff |
annotate
|
| Thu, 22 Dec 2005 00:29:04 +0100 |
wenzelm |
CONJUNCTS2;
|
file |
diff |
annotate
|
| Wed, 21 Dec 2005 13:25:20 +0100 |
haftmann |
discontinued unflat in favour of burrow and burrow_split
|
file |
diff |
annotate
|
| Fri, 16 Dec 2005 15:52:05 +0100 |
haftmann |
re-arranged tuples (theory * 'a) to ('a * theory) in Pure
|
file |
diff |
annotate
|
| Fri, 09 Dec 2005 09:06:45 +0100 |
haftmann |
oriented result pairs in PureThy
|
file |
diff |
annotate
|
| Tue, 06 Dec 2005 09:04:09 +0100 |
haftmann |
re-oriented some result tuples in PureThy
|
file |
diff |
annotate
|
| Fri, 02 Dec 2005 22:57:36 +0100 |
wenzelm |
defines: beta/eta contract lhs;
|
file |
diff |
annotate
|
| Fri, 02 Dec 2005 08:06:59 +0100 |
haftmann |
introduced new map2, fold
|
file |
diff |
annotate
|
| Sat, 19 Nov 2005 14:22:28 +0100 |
wenzelm |
CONJUNCTS;
|
file |
diff |
annotate
|
| Wed, 16 Nov 2005 17:45:36 +0100 |
wenzelm |
tuned Pattern.match/unify;
|
file |
diff |
annotate
|
| Wed, 09 Nov 2005 16:26:52 +0100 |
wenzelm |
moved datatype elem to element.ML;
|
file |
diff |
annotate
|
| Tue, 08 Nov 2005 10:43:15 +0100 |
wenzelm |
avoid prove_plain, export_plain, simplified after_qed;
|
file |
diff |
annotate
|
| Fri, 28 Oct 2005 22:28:09 +0200 |
wenzelm |
tuned ProofContext.export interfaces;
|
file |
diff |
annotate
|
| Fri, 21 Oct 2005 18:14:53 +0200 |
wenzelm |
Goal.prove_plain;
|
file |
diff |
annotate
|
| Tue, 18 Oct 2005 17:59:34 +0200 |
wenzelm |
ObjectLogic.atomize_cterm;
|
file |
diff |
annotate
|
| Sat, 15 Oct 2005 00:08:05 +0200 |
wenzelm |
goal statements: accomodate before_qed argument;
|
file |
diff |
annotate
|
| Tue, 04 Oct 2005 19:01:37 +0200 |
wenzelm |
minor tweaks for Poplog/ML;
|
file |
diff |
annotate
|
| Tue, 20 Sep 2005 08:21:49 +0200 |
haftmann |
slight adaptions to library changes
|
file |
diff |
annotate
|
| Mon, 19 Sep 2005 16:38:35 +0200 |
haftmann |
introduced AList module
|
file |
diff |
annotate
|
| Sat, 17 Sep 2005 12:18:05 +0200 |
wenzelm |
interpretation: use goal commands without target -- no storing of results;
|
file |
diff |
annotate
|
| Fri, 16 Sep 2005 16:07:22 +0200 |
ballarin |
tuned
|
file |
diff |
annotate
|
| Fri, 16 Sep 2005 14:46:31 +0200 |
ballarin |
interpretation uses primitive goal interface
|
file |
diff |
annotate
|
| Thu, 15 Sep 2005 17:16:56 +0200 |
wenzelm |
TableFun/Symtab: curried lookup and update;
|
file |
diff |
annotate
|
| Wed, 14 Sep 2005 22:04:35 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 13 Sep 2005 22:19:39 +0200 |
wenzelm |
load late, after proof.ML;
|
file |
diff |
annotate
|
| Fri, 09 Sep 2005 12:18:15 +0200 |
ballarin |
fixed printing of locales
|
file |
diff |
annotate
|
| Tue, 06 Sep 2005 08:30:43 +0200 |
haftmann |
introduced some new-style AList operations
|
file |
diff |
annotate
|
| Mon, 05 Sep 2005 08:14:35 +0200 |
haftmann |
introduced binding priority 1 for linear combinators etc.
|
file |
diff |
annotate
|
| Fri, 02 Sep 2005 09:50:58 +0200 |
ballarin |
print_locale omits facts by default
|
file |
diff |
annotate
|
| Thu, 01 Sep 2005 18:48:50 +0200 |
wenzelm |
curried_lookup/update;
|
file |
diff |
annotate
|
| Wed, 31 Aug 2005 15:46:40 +0200 |
wenzelm |
refer to theory instead of low-level tsig;
|
file |
diff |
annotate
|
| Thu, 25 Aug 2005 09:25:03 +0200 |
haftmann |
add_locale_context(_i) now exporting elements (still some refinements to be done)
|
file |
diff |
annotate
|
| Wed, 24 Aug 2005 12:05:48 +0200 |
ballarin |
Interpretation in locales: extended back end;
|
file |
diff |
annotate
|
| Thu, 18 Aug 2005 11:17:44 +0200 |
wenzelm |
added add_locale_context(_i), which returns the body context for presentation;
|
file |
diff |
annotate
|
| Wed, 17 Aug 2005 17:04:15 +0200 |
ballarin |
Improved generation of witnesses in interpretation.
|
file |
diff |
annotate
|
| Mon, 08 Aug 2005 22:11:31 +0200 |
ballarin |
Release of interpretation in locale.
|
file |
diff |
annotate
|
| Tue, 02 Aug 2005 16:52:21 +0200 |
ballarin |
First version of interpretation in locales. Not yet fully functional.
|
file |
diff |
annotate
|
| Thu, 28 Jul 2005 15:20:04 +0200 |
wenzelm |
Sign.typ_unify;
|
file |
diff |
annotate
|
| Fri, 15 Jul 2005 15:44:15 +0200 |
wenzelm |
tuned fold on terms;
|
file |
diff |
annotate
|
| Thu, 14 Jul 2005 19:28:34 +0200 |
wenzelm |
sys_error;
|
file |
diff |
annotate
|
| Wed, 13 Jul 2005 11:30:37 +0200 |
haftmann |
(fix for an accidental commit)
|
file |
diff |
annotate
|
| Wed, 13 Jul 2005 11:16:34 +0200 |
haftmann |
(intermediate commit)
|
file |
diff |
annotate
|
| Thu, 07 Jul 2005 15:52:31 +0200 |
ballarin |
Preparations for interpretation of locales in locales.
|
file |
diff |
annotate
|
| Thu, 30 Jun 2005 14:06:29 +0200 |
ballarin |
Proper treatment of beta-redexes in witness theorems.
|
file |
diff |
annotate
|
| Fri, 17 Jun 2005 18:35:27 +0200 |
wenzelm |
accomodate change of TheoryDataFun;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2005 12:03:33 +0200 |
wenzelm |
NameSpace.extern_table;
|
file |
diff |
annotate
|
| Wed, 08 Jun 2005 16:11:09 +0200 |
ballarin |
Fixed "axiom" generation for mixed locales with and without predicates.
|
file |
diff |
annotate
|
| Wed, 01 Jun 2005 12:30:50 +0200 |
ballarin |
Locales: new element constrains, parameter renaming with syntax,
|
file |
diff |
annotate
|
| Tue, 31 May 2005 11:53:35 +0200 |
wenzelm |
renamed cond_extern to extern;
|
file |
diff |
annotate
|
| Fri, 27 May 2005 17:10:41 +0200 |
ballarin |
SML/NJ compatibility.
|
file |
diff |
annotate
|
| Fri, 27 May 2005 16:33:33 +0200 |
ballarin |
Deleted old code.
|
file |
diff |
annotate
|
| Fri, 27 May 2005 16:24:48 +0200 |
ballarin |
Locale expressions: rename with optional mixfix syntax.
|
file |
diff |
annotate
|
| Sun, 22 May 2005 16:51:16 +0200 |
wenzelm |
fold ProofContext.declare_term;
|
file |
diff |
annotate
|
| Tue, 26 Apr 2005 17:44:24 +0200 |
paulson |
eta-expanded a function
|
file |
diff |
annotate
|
| Tue, 26 Apr 2005 09:24:58 +0200 |
ballarin |
Fixed bug in fact activation.
|
file |
diff |
annotate
|
| Mon, 25 Apr 2005 17:58:41 +0200 |
ballarin |
Subsumption of locale interpretations.
|
file |
diff |
annotate
|
| Thu, 21 Apr 2005 22:02:06 +0200 |
wenzelm |
superceded by Pure.thy and CPure.thy;
|
file |
diff |
annotate
|
| Thu, 21 Apr 2005 19:13:03 +0200 |
berghofe |
Adapted to new interface of instantiation and unification / matching functions.
|
file |
diff |
annotate
|
| Mon, 18 Apr 2005 09:25:23 +0200 |
ballarin |
Interpretation supports statically scoped attributes; documentation.
|
file |
diff |
annotate
|
| Sat, 16 Apr 2005 18:57:18 +0200 |
wenzelm |
tuned (t)inst_tab_elem;
|
file |
diff |
annotate
|
| Wed, 13 Apr 2005 18:49:07 +0200 |
wenzelm |
*** MESSAGE REFERS TO PREVIOUS VERSION ***
|
file |
diff |
annotate
|
| Wed, 13 Apr 2005 18:34:22 +0200 |
wenzelm |
*** empty log message ***
|
file |
diff |
annotate
|
| Mon, 11 Apr 2005 12:34:34 +0200 |
ballarin |
First release of interpretation commands.
|
file |
diff |
annotate
|
| Thu, 24 Mar 2005 17:03:37 +0100 |
ballarin |
Further work on interpretation commands. New command `interpret' for
|
file |
diff |
annotate
|
| Thu, 24 Mar 2005 16:36:40 +0100 |
ballarin |
*** empty log message ***
|
file |
diff |
annotate
|
| Thu, 10 Mar 2005 17:48:36 +0100 |
ballarin |
Registrations of global locale interpretations: improved, better naming.
|
file |
diff |
annotate
|
| Wed, 09 Mar 2005 18:44:52 +0100 |
ballarin |
First version of global registration command.
|
file |
diff |
annotate
|
| Fri, 04 Mar 2005 15:07:34 +0100 |
skalberg |
Removed practically all references to Library.foldr.
|
file |
diff |
annotate
|
| Thu, 03 Mar 2005 12:43:01 +0100 |
skalberg |
Move towards standard functions.
|
file |
diff |
annotate
|
| Sun, 13 Feb 2005 17:15:14 +0100 |
skalberg |
Deleted Library.option type.
|
file |
diff |
annotate
|
| Mon, 24 Jan 2005 17:56:18 +0100 |
berghofe |
Specific theorems in a named list of theorems can now be referred to
|
file |
diff |
annotate
|
| Tue, 28 Sep 2004 13:54:49 +0200 |
ballarin |
Bug fixes.
|
file |
diff |
annotate
|
| Mon, 27 Sep 2004 10:27:34 +0200 |
ballarin |
Modified locales: improved implementation of "includes".
|
file |
diff |
annotate
|
| Thu, 12 Aug 2004 10:01:09 +0200 |
ballarin |
Disallowed "includes" in locale declarations.
|
file |
diff |
annotate
|
| Tue, 03 Aug 2004 14:48:59 +0200 |
ballarin |
Typo.
|
file |
diff |
annotate
|
| Mon, 02 Aug 2004 10:16:58 +0200 |
ballarin |
Some comments added.
|
file |
diff |
annotate
|
| Mon, 21 Jun 2004 10:25:57 +0200 |
kleing |
Merged in license change from Isabelle2004
|
file |
diff |
annotate
|
| Fri, 21 May 2004 21:19:47 +0200 |
wenzelm |
TypeInfer.paramify_dummies, TypeInfer.param;
|
file |
diff |
annotate
|
| Sat, 01 May 2004 22:08:57 +0200 |
wenzelm |
improved Term.invent_names;
|
file |
diff |
annotate
|
| Thu, 22 Apr 2004 10:52:32 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 14 Apr 2004 13:28:46 +0200 |
wenzelm |
renamed have_thms to note_thms;
|
file |
diff |
annotate
|
| Wed, 07 Apr 2004 20:42:13 +0200 |
ballarin |
Locale instantiation: label parameter optional, new attribute paramter.
|
file |
diff |
annotate
|