Mercurial
Mercurial
>
hg
>
nominal2
/ file revisions
summary
|
shortlog
|
changelog
|
graph
|
tags
|
bookmarks
|
branches
|
file
| revisions |
annotate
|
diff
|
comparison
|
rss
|
help
(0)
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
Nominal-General/Nominal2_Eqvt.thy
2010-05-13
Christian Urban
added flip_eqvt and swap_eqvt to the equivariance lists
file
|
diff
|
annotate
2010-05-09
Christian Urban
added eqvt-lemma for split; changed semantics of perm_simp: excluded stands for constants about which no complaint is written out...eqvt_apply is now always applied
file
|
diff
|
annotate
2010-05-05
Christian Urban
solved the problem with equivariance by first eta-normalising the goal
file
|
diff
|
annotate
2010-05-02
Christian Urban
removed duplicate eqvt attribute
file
|
diff
|
annotate
2010-04-30
Christian Urban
added eqvt-lemmas for Bex, Ball and Union
file
|
diff
|
annotate
2010-04-30
Christian Urban
reorganised eqvt-file (now uses perm_simp already)
file
|
diff
|
annotate
2010-04-28
Christian Urban
simpliied and moved the remaining lemmas about the atom-function to Nominal2_Base
file
|
diff
|
annotate
2010-04-27
Christian Urban
moved mk_atom into the library; that meant that concrete atom classes need to be in Nominal2_Base
file
|
diff
|
annotate
2010-04-26
Christian Urban
rewrote eqvts_raw to be a symtab, that can be looked up
file
|
diff
|
annotate
2010-04-25
Christian Urban
tuned and cleaned
file
|
diff
|
annotate
2010-04-22
Christian Urban
tuned parser
file
|
diff
|
annotate
2010-04-22
Christian Urban
moved lemmas from FSet.thy to do with atom to Nominal2_Base, and to do with 'a::at set to Nominal2_Atoms; moved Nominal2_Eqvt.thy one up to be loaded before Nominal2_Atoms
file
|
diff
|
annotate
2010-04-18
Christian Urban
tuned
file
|
diff
|
annotate
2010-04-18
Christian Urban
tuned
file
|
diff
|
annotate
2010-04-18
Christian Urban
preliminary parser for perm_simp metod
file
|
diff
|
annotate
2010-04-16
Christian Urban
automatic proofs for equivariance of alphas
file
|
diff
|
annotate
2010-04-14
Christian Urban
tuned and removed dead code
file
|
diff
|
annotate
2010-04-14
Christian Urban
added a library for basic nominal functions; separated nominal_eqvt file
file
|
diff
|
annotate
2010-04-14
Christian Urban
deleted test
file
|
diff
|
annotate
2010-04-12
Christian Urban
moved equivariance of map into Nominal2_Eqvt file
file
|
diff
|
annotate
2010-04-12
Christian Urban
implemented in thmdecls the case where eqvt-lemmas are of the form _ ==> _
file
|
diff
|
annotate
2010-04-11
Christian Urban
fixed bug in thmdecls with destructing Trueprop; some initial infrastructure for eqvt-theorems of the form _ ==> _
file
|
diff
|
annotate
2010-04-11
Christian Urban
used warning instead of tracing (does not seem to produce stable output)
file
|
diff
|
annotate
2010-04-11
Christian Urban
added more robust tracing infrastructure; a strict version of the eqvt_tac raises an error if not all permutations cannot be analysed
file
|
diff
|
annotate
2010-04-09
Christian Urban
changed the eqvt-tac to move only outermost permutations inside; added tracing infrastructure for the eqvt-tac
file
|
diff
|
annotate
2010-04-04
Christian Urban
separated general nominal theory into separate folder
file
|
diff
|
annotate
|
base
less
more
(0)
tip