| Thu, 10 Apr 2014 17:48:18 +0200 |
setup for Transfer and Lifting from BNF; tuned thm names
|
file | diff | annotate |
| Thu, 10 Apr 2014 17:48:15 +0200 |
more appropriate name (Lifting.invariant -> eq_onp)
|
file | diff | annotate |
| Thu, 06 Mar 2014 15:40:33 +0100 |
renamed 'fun_rel' to 'rel_fun'
|
file | diff | annotate |
| Sat, 14 Dec 2013 17:28:05 +0100 |
proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.;
|
file | diff | annotate |
| Tue, 15 Jan 2013 17:28:46 +0100 |
avoid handling arbitrary exceptions, notably physical interrupts that would make the program erratic;
|
file | diff | annotate |
| Wed, 29 Aug 2012 11:48:45 +0200 |
renamed Position.str_of to Position.here;
|
file | diff | annotate |
| Wed, 16 May 2012 19:20:19 +0200 |
remove the generation of a code certificate from the Quotient package (mainly from quotient_def), because it's in lift_definition now
|
file | diff | annotate |
| Mon, 23 Apr 2012 17:18:18 +0200 |
move MRSL to a separate file
|
file | diff | annotate |
| Tue, 17 Apr 2012 14:56:38 +0200 |
go back to the explicit compisition of quotient theorems
|
file | diff | annotate |
| Tue, 10 Apr 2012 16:10:50 +0100 |
moved lift_raw_const wrapper out of the Quotient-package into Nominal2
|
file | diff | annotate |
| Thu, 05 Apr 2012 22:00:27 +0200 |
make Quotient_Def.lift_raw_const working again
|
file | diff | annotate |
| Tue, 03 Apr 2012 16:26:48 +0200 |
new package Lifting - initial commit
|
file | diff | annotate |
| Thu, 29 Mar 2012 21:13:48 +0200 |
use qualified names for rsp and rep_eq theorems in quotient_def
|
file | diff | annotate |
| Wed, 28 Mar 2012 10:44:04 +0200 |
some tuning while reviewing the current state of the quotient_def package
|
file | diff | annotate |
| Tue, 27 Mar 2012 14:46:34 +0200 |
note a code eqn in quotient_def
|
file | diff | annotate |
| Fri, 23 Mar 2012 14:25:31 +0100 |
generation of a code certificate from a respectfulness theorem for constants lifted by the quotient_definition command & setup_lifting command: setups Quotient infrastructure from a typedef theorem
|
file | diff | annotate |
| Fri, 23 Mar 2012 14:03:58 +0100 |
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
|
file | diff | annotate |
| Fri, 16 Mar 2012 18:20:12 +0100 |
outer syntax command definitions based on formal command_spec derived from theory header declarations;
|
file | diff | annotate |
| Thu, 15 Mar 2012 20:07:00 +0100 |
prefer formally checked @{keyword} parser;
|
file | diff | annotate |
| Tue, 13 Mar 2012 20:04:24 +0100 |
more explicit indication of def names;
|
file | diff | annotate |
| Tue, 20 Dec 2011 17:40:21 +0100 |
removing some debug output in quotient_definition
|
file | diff | annotate |
| Tue, 13 Dec 2011 14:04:20 +0100 |
support phantom types as quotient types
|
file | diff | annotate |
| Fri, 09 Dec 2011 14:14:37 +0100 |
make ctxt the first parameter
|
file | diff | annotate |
| Sun, 20 Nov 2011 17:04:59 +0100 |
more uniform signature;
|
file | diff | annotate |
| Fri, 28 Oct 2011 23:10:44 +0200 |
more robust data storage (NB: the morphism can change the shape of qconst, and in the auxiliary context it is not even a constant yet);
|
file | diff | annotate |
| Fri, 28 Oct 2011 22:17:30 +0200 |
uniform Local_Theory.declaration with explicit params;
|
file | diff | annotate |
| Thu, 27 Oct 2011 20:26:38 +0200 |
simplified/standardized signatures;
|
file | diff | annotate |
| Tue, 05 Jul 2011 09:54:39 +0200 |
re-check to explicitly propagate a given type constraint to lhs -- necessary to trigger type improvement in an instantiation target
|
file | diff | annotate |
| Thu, 30 Jun 2011 10:15:46 +0200 |
parse term in auxiliary context augmented with variable;
|
file | diff | annotate |
| Wed, 27 Apr 2011 20:58:40 +0200 |
tuned signature -- eliminated odd comment;
|
file | diff | annotate |
| Sat, 16 Apr 2011 12:46:18 +0200 |
tuned signature, disentangled dependencies;
|
file | diff | annotate |
| Fri, 07 Jan 2011 21:26:49 +0100 |
do not open ML structures;
|
file | diff | annotate |
| Fri, 07 Jan 2011 15:35:00 +0100 |
more precise parentheses and indentation;
|
file | diff | annotate |
| Sun, 22 Aug 2010 10:45:53 +0800 |
changed to a more convenient argument order
|
file | diff | annotate |
| Thu, 08 Jul 2010 16:19:24 +0200 |
tuned titles
|
file | diff | annotate |
| Mon, 28 Jun 2010 16:20:39 +0100 |
separation of translations in derive_qtrm / derive_rtrm (similarly for types)
|
file | diff | annotate |
| Mon, 28 Jun 2010 09:48:36 +0200 |
Quotient package reverse lifting
|
file | diff | annotate |
| Mon, 28 Jun 2010 07:38:39 +0200 |
Add reverse lifting flag to automated theorem derivation
|
file | diff | annotate |
| Mon, 28 Jun 2010 07:32:51 +0200 |
Restrict quotient definitions to constants
|
file | diff | annotate |
| Sun, 27 Jun 2010 08:33:01 +0100 |
mixfix can be given for automatically lifted constants
|
file | diff | annotate |
| Thu, 24 Jun 2010 16:27:40 +0100 |
slight cleaning and simplification of the automatic wrapper for quotient definitions
|
file | diff | annotate |
| Thu, 24 Jun 2010 12:33:51 +0100 |
export of proper information in the ML-interface of the quotient package
|
file | diff | annotate |
| Mon, 17 May 2010 23:54:15 +0200 |
prefer structure Keyword, Parse, Parse_Spec, Outer_Syntax;
|
file | diff | annotate |
| Sun, 16 May 2010 00:02:11 +0200 |
prefer structure Parse_Spec;
|
file | diff | annotate |
| Sun, 11 Apr 2010 15:42:05 +0200 |
stay within Local_Defs layer;
|
file | diff | annotate |
| Sat, 27 Mar 2010 14:48:46 +0100 |
Automated lifting can be restricted to specific quotient types
|
file | diff | annotate |
| Sun, 14 Mar 2010 14:31:24 +0100 |
observe standard header format;
|
file | diff | annotate |
| Sun, 07 Mar 2010 11:57:16 +0100 |
modernized structure Local_Defs;
|
file | diff | annotate |
| Fri, 19 Feb 2010 13:54:19 +0100 |
Initial version of HOL quotient package.
|
file | diff | annotate |