| 2016-06-22 |
wenzelm |
bundle lifting_syntax;
|
file |
diff |
annotate
|
| 2015-12-07 |
wenzelm |
isabelle update_cartouches -c -t;
|
file |
diff |
annotate
|
| 2015-07-18 |
wenzelm |
isabelle update_cartouches;
|
file |
diff |
annotate
|
| 2014-11-22 |
wenzelm |
named_theorems: multiple args;
|
file |
diff |
annotate
|
| 2014-11-02 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| 2014-08-16 |
wenzelm |
updated to named_theorems;
|
file |
diff |
annotate
|
| 2014-03-13 |
nipkow |
enhanced simplifier solver for preconditions of rewrite rule, can now deal with conjunctions
|
file |
diff |
annotate
|
| 2014-03-06 |
blanchet |
renamed 'fun_rel' to 'rel_fun'
|
file |
diff |
annotate
|
| 2013-12-26 |
haftmann |
prefer ephemeral interpretation over interpretation in proof contexts;
|
file |
diff |
annotate
|
| 2013-11-21 |
blanchet |
rationalize imports
|
file |
diff |
annotate
|
| 2013-08-13 |
kuncar |
introduce locale with syntax for fun_rel and map_fun and make thus ===> and ---> local
|
file |
diff |
annotate
|
| 2013-02-14 |
haftmann |
abandoned theory Plain
|
file |
diff |
annotate
|
| 2012-08-22 |
wenzelm |
prefer ML_file over old uses;
|
file |
diff |
annotate
|
| 2012-04-20 |
huffman |
move definition of set_rel into Library/Quotient_Set.thy
|
file |
diff |
annotate
|
| 2012-04-19 |
huffman |
tuned lemmas (v)image_id;
|
file |
diff |
annotate
|
| 2012-04-18 |
huffman |
move constant 'Respects' into Lifting.thy;
|
file |
diff |
annotate
|
| 2012-04-15 |
haftmann |
centralized enriched_type declaration, thanks to in-situ available Isar commands
|
file |
diff |
annotate
|
| 2012-04-12 |
bulwahn |
merged
|
file |
diff |
annotate
|
| 2012-04-04 |
griff |
manual merge
|
file |
diff |
annotate
|
| 2012-04-03 |
griff |
dropped abbreviation "pred_comp"; introduced infix notation "P OO Q" for "relcompp P Q"
|
file |
diff |
annotate
|
| 2012-04-04 |
kuncar |
connect the Quotient package to the Lifting package
|
file |
diff |
annotate
|
| 2012-04-04 |
kuncar |
support non-open typedefs; define cr_rel in terms of a rep function for typedefs
|
file |
diff |
annotate
|
| 2012-04-03 |
kuncar |
new package Lifting - initial commit
|
file |
diff |
annotate
|
| 2012-03-23 |
kuncar |
hide invariant constant
|
file |
diff |
annotate
|
| 2012-03-23 |
kuncar |
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
|
| 2012-03-23 |
kuncar |
store the relational theorem for every relator
|
file |
diff |
annotate
|
| 2012-03-23 |
kuncar |
respectfulness theorem has to be proved if a new constant is lifted by quotient_definition
|
file |
diff |
annotate
|
| 2012-03-15 |
wenzelm |
declare command keywords via theory header, including strict checking outside Pure;
|
file |
diff |
annotate
|
| 2012-03-15 |
wenzelm |
declare minor keywords via theory header;
|
file |
diff |
annotate
|
| 2012-02-14 |
wenzelm |
simplified use of tacticals;
|
file |
diff |
annotate
|
| 2011-12-24 |
haftmann |
treatment of type constructor `set`
|
file |
diff |
annotate
|
| 2011-12-09 |
kuncar |
Quotient_Info stores only relation maps
|
file |
diff |
annotate
|
| 2011-12-07 |
Christian Urban |
added a specific tactic and method that deal with partial equivalence relations
|
file |
diff |
annotate
|
| 2011-11-29 |
wenzelm |
more conventional file name;
|
file |
diff |
annotate
|
| 2011-09-14 |
huffman |
tuned proofs
|
file |
diff |
annotate
|
| 2011-08-26 |
haftmann |
avoid intermixing set and predicates; dropped lemmas mem_rsp and mem_prs (now in Quotient_Set.thy)
|
file |
diff |
annotate
|
| 2011-08-22 |
Cezary Kaliszyk |
Quotient Package: some infrastructure for lifting inside sets
|
file |
diff |
annotate
|
| 2011-08-16 |
haftmann |
avoid Collect_def in proof
|
file |
diff |
annotate
|
| 2011-08-15 |
Cezary Kaliszyk |
Quotient Package: make quotient_type work with separate set type
|
file |
diff |
annotate
|
| 2011-05-15 |
wenzelm |
simplified/unified method_setup/attribute_setup;
|
file |
diff |
annotate
|
| 2011-04-14 |
blanchet |
use old Skolemizer for Metis call that requires high unification bound (around 100) with the new Skolemizer
|
file |
diff |
annotate
|
| 2011-03-13 |
wenzelm |
tuned headers;
|
file |
diff |
annotate
|
| 2011-01-07 |
wenzelm |
more standard package setup;
|
file |
diff |
annotate
|
| 2010-11-29 |
haftmann |
reorienting iff in Quotient_rel prevents simplifier looping;
|
file |
diff |
annotate
|
| 2010-11-29 |
haftmann |
moved generic definitions about (partial) equivalence relations from Quotient to Equiv_Relations;
|
file |
diff |
annotate
|
| 2010-11-19 |
haftmann |
generalized type
|
file |
diff |
annotate
|
| 2010-11-18 |
haftmann |
map_fun combinator in theory Fun
|
file |
diff |
annotate
|
| 2010-11-09 |
haftmann |
type annotations in specifications; fun_rel_def is no simp rule by default; slightly changed fun_map_def; more on predicates on relation functions; proper HOL equations in definitions
|
file |
diff |
annotate
|
| 2010-10-19 |
Cezary Kaliszyk |
Quotient package: partial equivalence introduction
|
file |
diff |
annotate
|
| 2010-10-05 |
blanchet |
remove needless Metis facts
|
file |
diff |
annotate
|
| 2010-10-04 |
blanchet |
move Metis into Plain
|
file |
diff |
annotate
|
| 2010-09-24 |
Cezary Kaliszyk |
quotient package: respectfulness and preservation of identity.
|
file |
diff |
annotate
|
| 2010-09-13 |
nipkow |
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
|
file |
diff |
annotate
|
| 2010-09-07 |
nipkow |
expand_fun_eq -> ext_iff
|
file |
diff |
annotate
|
| 2010-08-30 |
Cezary Kaliszyk |
Quotient Package: added respectfulness and preservation lemmas for mem.
|
file |
diff |
annotate
|
| 2010-08-28 |
Christian Urban |
quotient package: lemmas to be lifted and descended can be pre-simplified
|
file |
diff |
annotate
|
| 2010-08-25 |
Cezary Kaliszyk |
Quotient Package / lemma for regularization of bex1_rel for equivalence relations
|
file |
diff |
annotate
|
| 2010-08-11 |
Christian Urban |
deleted duplicate lemma
|
file |
diff |
annotate
|
| 2010-07-27 |
wenzelm |
use file names relative to master directory of theory source -- Proof General can now handle that due to the ThyLoad.add_path deception (cf. 3ceccd415145);
|
file |
diff |
annotate
|
| 2010-06-29 |
Christian Urban |
separated the lifting and descending procedures in the quotient package
|
file |
diff |
annotate
|