Tue, 26 Aug 2008 16:04:22 +0200 |
Reorganisation of registration code.
|
file | diff | annotate |
Thu, 14 Aug 2008 16:52:46 +0200 |
moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
|
file | diff | annotate |
Wed, 06 Aug 2008 16:41:40 +0200 |
Interpretation command (theory/proof context) no longer simplifies goal.
|
file | diff | annotate |
Fri, 01 Aug 2008 17:41:37 +0200 |
Removed import and lparams from locale record.
|
file | diff | annotate |
Wed, 30 Jul 2008 07:33:59 +0200 |
facts_of
|
file | diff | annotate |
Tue, 29 Jul 2008 08:15:44 +0200 |
tuned; explicit export of element accessors
|
file | diff | annotate |
Sat, 26 Jul 2008 09:00:26 +0200 |
tuned function name
|
file | diff | annotate |
Fri, 25 Jul 2008 12:03:32 +0200 |
dropped locale (open)
|
file | diff | annotate |
Sun, 18 May 2008 15:04:41 +0200 |
Syntax.string_of_typ: proper context;
|
file | diff | annotate |
Mon, 14 Apr 2008 17:54:56 +0200 |
Changed naming scheme for theorems generated by interpretations.
|
file | diff | annotate |
Sat, 12 Apr 2008 17:00:48 +0200 |
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 |
Context.>> : operate on Context.generic;
|
file | diff | annotate |
Thu, 27 Mar 2008 15:32:15 +0100 |
eliminated delayed theory setup
|
file | diff | annotate |
Thu, 20 Mar 2008 00:20:49 +0100 |
renamed former get_thms(_silent) to get_fact(_silent);
|
file | diff | annotate |
Mon, 17 Mar 2008 18:36:04 +0100 |
closeup: recover original order of free variables!
|
file | diff | annotate |
Wed, 05 Mar 2008 22:58:11 +0100 |
closeup: minor tuning of term traversal;
|
file | diff | annotate |
Mon, 17 Dec 2007 17:57:52 +0100 |
explicit closing of derived witnesses
|
file | diff | annotate |
Thu, 13 Dec 2007 07:09:07 +0100 |
memorizing and exporting destruction rules
|
file | diff | annotate |
Thu, 08 Nov 2007 22:19:43 +0100 |
avoid "import" as identifier, which is a keyword in Alice;
|
file | diff | annotate |
Mon, 05 Nov 2007 17:48:51 +0100 |
Use of export rather than standard in interpretation.
|
file | diff | annotate |
Fri, 02 Nov 2007 18:53:01 +0100 |
generic tactic Method.intros_tac
|
file | diff | annotate |
Fri, 19 Oct 2007 12:22:12 +0200 |
Interpretation equations may have name and/or attribute;
|
file | diff | annotate |
Wed, 17 Oct 2007 23:16:34 +0200 |
locale pred: authentic syntax, tuned aprop_tr' accordingly;
|
file | diff | annotate |
Wed, 17 Oct 2007 13:55:37 +0200 |
clarified naming conventions of 'parse' and 'check' (as opposed to former 'cert');
|
file | diff | annotate |
Mon, 15 Oct 2007 15:29:43 +0200 |
canonical interpretation interface
|
file | diff | annotate |
Fri, 12 Oct 2007 14:42:30 +0200 |
tuned
|
file | diff | annotate |
Wed, 10 Oct 2007 17:32:00 +0200 |
removed redundant strip_vars/abs_eqn, use improved Drule.abs_def instead;
|
file | diff | annotate |
Wed, 10 Oct 2007 10:55:37 +0200 |
Prepare proper interface of interpretation_i, interpret_i.
|
file | diff | annotate |
Tue, 09 Oct 2007 00:20:13 +0200 |
generic Syntax.pretty/string_of operations;
|
file | diff | annotate |
Mon, 01 Oct 2007 12:24:07 +0200 |
Theory/context data restructured; simplified interface for printing of interpretations.
|
file | diff | annotate |
Sat, 29 Sep 2007 08:58:56 +0200 |
exported intern_expr
|
file | diff | annotate |
Mon, 24 Sep 2007 21:07:38 +0200 |
eliminated ProofContext.read_termTs;
|
file | diff | annotate |
Tue, 18 Sep 2007 18:50:17 +0200 |
Morphisms applied in global interpretations behave correctly on types and terms.
|
file | diff | annotate |
Tue, 04 Sep 2007 14:32:29 +0200 |
Improved comment.
|
file | diff | annotate |
Sat, 28 Jul 2007 20:40:24 +0200 |
tuned signature;
|
file | diff | annotate |
Fri, 27 Jul 2007 20:11:49 +0200 |
Druke.dummy_thm;
|
file | diff | annotate |
Mon, 23 Jul 2007 13:47:48 +0200 |
interpretation: unfolding of equations;
|
file | diff | annotate |
Sun, 08 Jul 2007 19:51:58 +0200 |
replaced exception TableFun/GraphFun.DUPS by TableFun/GraphFun.DUP;
|
file | diff | annotate |
Thu, 05 Jul 2007 20:01:28 +0200 |
simplified ObjectLogic.atomize;
|
file | diff | annotate |
Tue, 19 Jun 2007 23:15:27 +0200 |
balanced conjunctions;
|
file | diff | annotate |
Sun, 03 Jun 2007 23:16:56 +0200 |
added gen_merge_lists/merge_lists/merge_alists (legacy operations from library.ML);
|
file | diff | annotate |
Thu, 31 May 2007 23:47:36 +0200 |
simplified/unified list fold;
|
file | diff | annotate |
Mon, 07 May 2007 00:49:59 +0200 |
simplified DataFun interfaces;
|
file | diff | annotate |
Thu, 26 Apr 2007 12:00:05 +0200 |
renamed some old names Theory.xxx to Sign.xxx;
|
file | diff | annotate |
Mon, 23 Apr 2007 20:44:11 +0200 |
read_instantiations: proper type-inference with fixed variables, infer parameter types as well;
|
file | diff | annotate |
Fri, 20 Apr 2007 16:54:57 +0200 |
Interpretation equations applied to attributes;
|
file | diff | annotate |
Sun, 15 Apr 2007 14:32:00 +0200 |
Thm.fold_terms;
|
file | diff | annotate |
Sat, 14 Apr 2007 17:36:05 +0200 |
Term.string_of_vname;
|
file | diff | annotate |
Fri, 13 Apr 2007 10:01:43 +0200 |
Experimental interpretation code for definitions.
|
file | diff | annotate |
Tue, 03 Apr 2007 19:24:19 +0200 |
avoid clash with Alice keywords;
|
file | diff | annotate |
Mon, 26 Mar 2007 14:53:06 +0200 |
exported interface for intro rules
|
file | diff | annotate |
Fri, 23 Feb 2007 08:39:24 +0100 |
locale: add_locale accepts explicit predicate name, interpretation supports non-mandatory prefixes
|
file | diff | annotate |
Mon, 19 Feb 2007 16:44:08 +0100 |
more precise error message in parameter unification
|
file | diff | annotate |
Sat, 10 Feb 2007 09:26:19 +0100 |
internal interfaces for interpretation and interpret
|
file | diff | annotate |
Sun, 04 Feb 2007 22:02:21 +0100 |
interpretation: attempt to be more serious about name_morphism;
|
file | diff | annotate |
Sat, 30 Dec 2006 16:08:00 +0100 |
removed conditional combinator;
|
file | diff | annotate |
Thu, 07 Dec 2006 23:16:55 +0100 |
reorganized structure Tactic vs. MetaSimplifier;
|
file | diff | annotate |
Thu, 07 Dec 2006 17:58:52 +0100 |
tuned print_locale output;
|
file | diff | annotate |
Wed, 06 Dec 2006 21:19:03 +0100 |
export: added explicit term operation;
|
file | diff | annotate |
Tue, 05 Dec 2006 22:14:50 +0100 |
encode declarations as notes (attributes), which enables proper inheritance, interpretation etc.;
|
file | diff | annotate |