| Wed, 22 Jan 2025 22:22:19 +0100 |
wenzelm |
misc tuning: more concise operations on prems (without change of exceptions);
|
file |
diff |
annotate
|
| Thu, 08 Aug 2024 16:23:30 +0200 |
wenzelm |
tuned signature: more operations;
|
file |
diff |
annotate
|
| Thu, 08 Aug 2024 16:03:34 +0200 |
wenzelm |
tuned: more antiquotations;
|
file |
diff |
annotate
|
| Sun, 04 Aug 2024 13:24:54 +0200 |
wenzelm |
tuned: more explicit dest_Type_name and dest_Type_args;
|
file |
diff |
annotate
|
| Fri, 10 Sep 2021 14:59:19 +0200 |
wenzelm |
clarified signature: more scalable operations;
|
file |
diff |
annotate
|
| Tue, 04 Jun 2019 16:47:05 +0200 |
wenzelm |
proper context;
|
file |
diff |
annotate
|
| Tue, 04 Jun 2019 15:14:56 +0200 |
wenzelm |
misc tuning and clarification, notably wrt. flow of context;
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Mon, 27 Jul 2015 17:44:55 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 05 Jul 2015 15:02:30 +0200 |
wenzelm |
simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
|
file |
diff |
annotate
|
| Sun, 03 May 2015 14:35:48 +0200 |
wenzelm |
make SML/NJ more happy;
|
file |
diff |
annotate
|
| Tue, 18 Nov 2014 16:19:57 +0100 |
kuncar |
parametrize liting of terms by quotients
|
file |
diff |
annotate
|
| Tue, 18 Nov 2014 16:19:57 +0100 |
kuncar |
generalize prove_schematic_quot_thm
|
file |
diff |
annotate
|
| Sun, 29 Mar 2015 23:08:03 +0200 |
wenzelm |
clarified equality of formal entities;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 23:38:59 +0100 |
wenzelm |
clarified context;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 15:58:56 +0100 |
wenzelm |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 22:05:01 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 04 Mar 2015 19:53:18 +0100 |
wenzelm |
tuned signature -- prefer qualified names;
|
file |
diff |
annotate
|
| Tue, 10 Feb 2015 14:48:26 +0100 |
wenzelm |
proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
|
file |
diff |
annotate
|
| Thu, 24 Jul 2014 20:21:34 +0200 |
kuncar |
store explicitly quotient types with no_code => more precise registration of code equations
|
file |
diff |
annotate
|
| Tue, 25 Feb 2014 15:02:19 +0100 |
kuncar |
rewrite composition of quotients to a more readable form in a respectfulness goal that is presented to a user
|
file |
diff |
annotate
|
| Thu, 13 Feb 2014 15:51:54 +0100 |
kuncar |
more precise descripiton
|
file |
diff |
annotate
|
| Thu, 13 Feb 2014 14:32:04 +0100 |
kuncar |
don't catch QOUT_THM_INTERNAL from the recursive call of parametrize_relation_conv
|
file |
diff |
annotate
|
| Wed, 12 Feb 2014 18:32:55 +0100 |
kuncar |
Lifting: support a type variable as a raw type
|
file |
diff |
annotate
|
| Wed, 08 Jan 2014 16:59:57 +0100 |
kuncar |
ensure that schematic type variables are fresh in rty
|
file |
diff |
annotate
|
| Wed, 08 Jan 2014 12:05:42 +0100 |
kuncar |
ensure that the raw type of an abstract type cannot be treated as an abstract type recursively
|
file |
diff |
annotate
|
| Mon, 14 Oct 2013 15:01:41 +0200 |
kuncar |
update documentation of important public ML functions in Lifting
|
file |
diff |
annotate
|
| Mon, 16 Sep 2013 15:30:17 +0200 |
kuncar |
restoring Transfer/Lifting context
|
file |
diff |
annotate
|
| Wed, 28 Aug 2013 14:37:35 +0200 |
kuncar |
use only one data slot; rename print_quotmaps to print_quot_maps; tuned
|
file |
diff |
annotate
|
| Fri, 08 Mar 2013 13:14:23 +0100 |
kuncar |
lift_definition and setup_lifting generate parametric transfer rules if parametricity theorems are provided
|
file |
diff |
annotate
|
| Thu, 29 Nov 2012 17:54:20 +0100 |
kuncar |
parametrized correspondence relation: more robust procedure - don't ignore sorts; tuned
|
file |
diff |
annotate
|
| Mon, 26 Nov 2012 14:20:51 +0100 |
kuncar |
generate a parameterized correspondence relation
|
file |
diff |
annotate
|
| Mon, 21 May 2012 16:36:48 +0200 |
kuncar |
quot_del attribute, it allows us to deregister quotient types
|
file |
diff |
annotate
|
| Wed, 02 May 2012 19:02:16 +0200 |
kuncar |
resolved maxidx bug
|
file |
diff |
annotate
|
| Wed, 02 May 2012 18:26:10 +0200 |
kuncar |
documentation of the Lifting package on the ML level & tuned
|
file |
diff |
annotate
|
| Thu, 26 Apr 2012 12:03:11 +0200 |
kuncar |
support Quotient map theorems with invariant parameters
|
file |
diff |
annotate
|
| Thu, 26 Apr 2012 12:01:58 +0200 |
kuncar |
use a quot_map theorem attribute instead of the complicated map attribute
|
file |
diff |
annotate
|
| Mon, 23 Apr 2012 17:18:18 +0200 |
kuncar |
move MRSL to a separate file
|
file |
diff |
annotate
|
| Tue, 17 Apr 2012 14:56:38 +0200 |
kuncar |
go back to the explicit compisition of quotient theorems
|
file |
diff |
annotate
|
| Fri, 06 Apr 2012 14:39:27 +0200 |
huffman |
more robust generation of quotient rules using tactics
|
file |
diff |
annotate
|
| Fri, 06 Apr 2012 10:37:46 +0200 |
huffman |
add function dest_Quotient
|
file |
diff |
annotate
|
| Thu, 05 Apr 2012 23:22:54 +0200 |
kuncar |
detect incorrect situations; better error messages; sanity check for quot_thm in setup_lifting_infr
|
file |
diff |
annotate
|
| Wed, 04 Apr 2012 13:41:38 +0200 |
huffman |
prove_quot_theorem fixes types
|
file |
diff |
annotate
|
| Tue, 03 Apr 2012 16:26:48 +0200 |
kuncar |
new package Lifting - initial commit
|
file |
diff |
annotate
|