Tue, 25 Feb 2014 19:07:40 +0100 |
kuncar |
new rule for making rsp theorem more readable
|
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, 20 Feb 2014 16:56:33 +0100 |
kuncar |
refactoring; generate rep_eq always, not only when it would be accepted by the code generator
|
file |
diff |
annotate
|
Thu, 20 Feb 2014 15:14:37 +0100 |
noschinl |
less flex-flex pairs
|
file |
diff |
annotate
|
Tue, 18 Feb 2014 23:03:47 +0100 |
kuncar |
implement the reflexivity prover as a monotonicity prover that proves R >= op=; derive "reflexivity" rules for relators from mono rules and eq rules
|
file |
diff |
annotate
|
Mon, 20 Jan 2014 20:21:12 +0100 |
blanchet |
move BNF_LFP up the dependency chain
|
file |
diff |
annotate
|
Fri, 27 Sep 2013 14:43:26 +0200 |
kuncar |
new parametricity rules and useful lemmas
|
file |
diff |
annotate
|
Fri, 27 Sep 2013 09:07:45 +0200 |
Andreas Lochbihler |
add lemmas
|
file |
diff |
annotate
|
Thu, 26 Sep 2013 15:50:33 +0200 |
Andreas Lochbihler |
add lemmas
|
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, 23 Aug 2013 00:12:20 +0200 |
kuncar |
remove OP
|
file |
diff |
annotate
|
Tue, 13 Aug 2013 15:59:22 +0200 |
kuncar |
introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
|
file |
diff |
annotate
|
Wed, 05 Jun 2013 15:21:52 +0200 |
kuncar |
more reflexivity rules (for OO)
|
file |
diff |
annotate
|
Thu, 16 May 2013 15:21:12 +0200 |
kuncar |
reflexivity rules for the function type and equality
|
file |
diff |
annotate
|
Wed, 15 May 2013 12:10:39 +0200 |
kuncar |
stronger reflexivity prover
|
file |
diff |
annotate
|
Mon, 13 May 2013 13:59:04 +0200 |
kuncar |
better support for domains in Lifting/Transfer = replace Domainp T by the actual invariant in a transferred goal
|
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, 14 Feb 2013 12:24:42 +0100 |
haftmann |
abandoned theory Plain
|
file |
diff |
annotate
|
Wed, 22 Aug 2012 22:55:41 +0200 |
wenzelm |
prefer ML_file over old uses;
|
file |
diff |
annotate
|
Thu, 24 May 2012 14:20:23 +0200 |
kuncar |
prove reflexivity also for the quotient composition relation; reflp_preserve renamed to reflexivity_rule
|
file |
diff |
annotate
|
Wed, 16 May 2012 19:17:20 +0200 |
kuncar |
generate abs_eq, use it as a code equation for total quotients; no_abs_code renamed to no_code; added no_code for quotient_type command
|
file |
diff |
annotate
|
Wed, 16 May 2012 19:15:45 +0200 |
kuncar |
infrastructure that makes possible to prove that a relation is reflexive
|
file |
diff |
annotate
|
Fri, 04 May 2012 17:12:37 +0200 |
huffman |
lifting package produces abs_eq_iff rules for total quotients
|
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
|
Sat, 21 Apr 2012 13:12:27 +0200 |
huffman |
move alternative definition lemmas into Lifting.thy;
|
file |
diff |
annotate
|
Sat, 21 Apr 2012 13:06:22 +0200 |
huffman |
tuned proofs
|
file |
diff |
annotate
|
Thu, 19 Apr 2012 08:45:13 +0200 |
huffman |
generate abs_induct rules for quotient types
|
file |
diff |
annotate
|
Wed, 18 Apr 2012 17:04:03 +0200 |
kuncar |
Lifting: generate more thms & note them & tuned
|
file |
diff |
annotate
|