Mercurial
Mercurial
>
hg
>
nominal2
/ graph
summary
|
shortlog
|
changelog
| graph |
tags
|
bookmarks
|
branches
|
files
|
help
less
more
|
(0)
-1000
-240
+240
+1000
tip
Find changesets by keywords (author, files, the commit message), revision number or hash, or
revset expression
.
The revision graph only works with JavaScript-enabled browsers.
merge
2010-05-12, by Cezary Kaliszyk
fvbv_rsp include prod_rel.simps
2010-05-12, by Cezary Kaliszyk
better ML-interface (returning only a list of theorems and a context)
2010-05-12, by Christian Urban
merge
2010-05-12, by Cezary Kaliszyk
Use raw_induct instead of induct
2010-05-12, by Cezary Kaliszyk
ingnored parameters in equivariance; added a proper interface to be called from ML
2010-05-12, by Christian Urban
properly exported defined bn-functions
2010-05-12, by Christian Urban
Include raw permutation definitions in eqvt
2010-05-11, by Cezary Kaliszyk
Declare alpha_gen_eqvt as eqvt and change the proofs that used 'eqvts[symmetric]'
2010-05-11, by Cezary Kaliszyk
a bit for the introduction of the q-paper
2010-05-11, by Christian Urban
added some of the quotient literature; a bit more to the qpaper
2010-05-11, by Christian Urban
fixed a problem with non-existant alphas2
2010-05-10, by Christian Urban
added comment about bind_set
2010-05-10, by Christian Urban
fixing bind_set problem
2010-05-10, by Christian Urban
merge
2010-05-10, by Cezary Kaliszyk
Term8 comment
2010-05-10, by Cezary Kaliszyk
merge
2010-05-10, by Cezary Kaliszyk
Restore set bindings in CoreHaskell
2010-05-10, by Cezary Kaliszyk
Recursive examples with relation composition
2010-05-10, by Cezary Kaliszyk
merge
2010-05-10, by Cezary Kaliszyk
prod_rel and prod_fv eqvt and mono
2010-05-10, by Cezary Kaliszyk
ExLetRec
2010-05-10, by Cezary Kaliszyk
merge
2010-05-10, by Cezary Kaliszyk
Parser changes for compound relations
2010-05-10, by Cezary Kaliszyk
merge
2010-05-10, by Cezary Kaliszyk
Use mk_compound_fv' and mk_compound_rel'
2010-05-10, by Cezary Kaliszyk
merge
2010-05-10, by Cezary Kaliszyk
Membership in a pair of lists.
2010-05-10, by Cezary Kaliszyk
Synchronize FSet with repository
2010-05-10, by Cezary Kaliszyk
tuned file names for examples
2010-05-09, by Christian Urban
cleaned up a bit the examples; added equivariance to all examples
2010-05-09, by Christian Urban
fixed the problem with alpha containing splits
2010-05-09, by 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
2010-05-09, by Christian Urban
Manually added some newer keywords from the distribution
2010-05-07, by Cezary Kaliszyk
Regularize experiments
2010-05-07, by Cezary Kaliszyk
alpha_eqvt_tac with prod_rel and prod_fv simps
2010-05-06, by Cezary Kaliszyk
mem => member
2010-05-06, by Cezary Kaliszyk
merge
2010-05-06, by Cezary Kaliszyk
Fixes for new Isabelle
2010-05-06, by Cezary Kaliszyk
compound versions with prod_rel and prod_fun, not made default yet.
2010-05-06, by Cezary Kaliszyk
prod_rel and prod_fv simps
2010-05-06, by Cezary Kaliszyk
mem => member
2010-05-06, by Cezary Kaliszyk
prod_rel.simps and Fixed for new isabelle
2010-05-06, by Cezary Kaliszyk
Fixes for new isabelle
2010-05-06, by Cezary Kaliszyk
prod_fv and its respectfullness and preservation.
2010-05-06, by Cezary Kaliszyk
Experiments with equivariance.
2010-05-06, by Cezary Kaliszyk
merged
2010-05-05, by Christian Urban
a bit mor on the pearl journal paper
2010-05-05, by Christian Urban
solved the problem with equivariance by first eta-normalising the goal
2010-05-05, by Christian Urban
Some cleaning in Term4
2010-05-05, by Cezary Kaliszyk
"isabelle make" compiles all examples with newparser/newfv/newalpha only.
2010-05-04, by Cezary Kaliszyk
Move Term4 to NewParser
2010-05-04, by Cezary Kaliszyk
Fix Term4 for permutation signature change
2010-05-04, by Cezary Kaliszyk
Move LF to NewParser. Just works.
2010-05-04, by Cezary Kaliszyk
merge
2010-05-04, by Cezary Kaliszyk
ExLetMult
2010-05-04, by Cezary Kaliszyk
Ex1Rec.
2010-05-04, by Cezary Kaliszyk
merge
2010-05-04, by Cezary Kaliszyk
merge
2010-05-04, by Cezary Kaliszyk
ExPS3 in NewParser
2010-05-04, by Cezary Kaliszyk
Move ExPS8 to new parser.
2010-05-04, by Cezary Kaliszyk
Fix for new isabelle
2010-05-04, by Cezary Kaliszyk
merge
2010-05-04, by Cezary Kaliszyk
Minor
2010-05-04, by Cezary Kaliszyk
increased step counter so that all steps go through
2010-05-04, by Christian Urban
fixed my error with define_raw_fv
2010-05-04, by Christian Urban
tuned and added some comments to the code; added also an exception for early exit of the nominal2_cmd function
2010-05-04, by Christian Urban
Separate Term8, as it may work soon.
2010-05-04, by Cezary Kaliszyk
moved CoreHaskell to NewParser.
2010-05-04, by Cezary Kaliszyk
ExPS7 in NewParser
2010-05-04, by Cezary Kaliszyk
Move ExLeroy to New Parser
2010-05-04, by Cezary Kaliszyk
Move 2 more to NewParser
2010-05-04, by Cezary Kaliszyk
Move TypeSchemes to NewParser
2010-05-04, by Cezary Kaliszyk
Move ExLet to NewParser.
2010-05-04, by Cezary Kaliszyk
tuned
2010-05-04, by Christian Urban
roll back of the last commit (there was a difference)
2010-05-04, by Christian Urban
tuned
2010-05-04, by Christian Urban
to my best knowledge the number of datatypes is equal to the length of the dt_descr; so we can save one argument in define_raw_perm
2010-05-04, by Christian Urban
merged
2010-05-04, by Christian Urban
some preliminary changes to the pearl-jv paper
2010-05-04, by Christian Urban
some preliminary notes of the abstract (qpaper); still need to see the motivating example
2010-05-03, by Christian Urban
Added cheats to classical
2010-05-03, by Cezary Kaliszyk
Ex2 moved to new parser.
2010-05-03, by Cezary Kaliszyk
alpha_eqvt_tac fixed to work when the existential is not at the top level.
2010-05-03, by Cezary Kaliszyk
SingleLet and Ex3 work with NewParser.
2010-05-03, by Cezary Kaliszyk
Comment
2010-05-03, by Cezary Kaliszyk
Another example where only alpha_eqvt fails.
2010-05-03, by Cezary Kaliszyk
Register only non-looping rules in eq_iff
2010-05-03, by Cezary Kaliszyk
Equivariance fails for single let?
2010-05-03, by Cezary Kaliszyk
NewParser
2010-05-03, by Cezary Kaliszyk
Introduce eq_iff_simp to match the one from Parser.
2010-05-03, by Cezary Kaliszyk
remove tracing
2010-05-03, by Cezary Kaliszyk
Cheat support equations in new parser
2010-05-03, by Cezary Kaliszyk
Remove dependency on NewFv
2010-05-03, by Cezary Kaliszyk
Fix Parser
2010-05-03, by Cezary Kaliszyk
Add explicit cheats in NewParser and comment out the examples for outside use.
2010-05-03, by Cezary Kaliszyk
Fix Datatype_Aux calls in NewParser.
2010-05-03, by Cezary Kaliszyk
Move old fv_alpha_export to Fv.
2010-05-03, by Cezary Kaliszyk
moved old parser and old fv back into their original places; isabelle make works again
2010-05-03, by Christian Urban
slight tuning
2010-05-03, by Christian Urban
simplified the supp-of-finite-sets proof
2010-05-02, by Christian Urban
tried to add some comments in the huge(!) nominal2_cmd function
2010-05-02, by Christian Urban
replaced make_pair with library function HOLogic.mk_prod
2010-05-02, by Christian Urban
removed duplicate eqvt attribute
2010-05-02, by Christian Urban
attempted to remove dependency on (old) Fv and (old) Parser; lifting still uses Fv.thy; the examples do not work at the moment (with equivp proofs failing)
2010-05-02, by Christian Urban
merged
2010-05-01, by Christian Urban
tuned
2010-05-01, by Christian Urban
replaced hide by the new hide_const
2010-04-30, by Christian Urban
generalised the fs-instance lemma (not just fsets of atoms are finitely supported, but also fsets of finitely supported elements)
2010-04-30, by Christian Urban
added lemmas establishing the support of finite sets of finitely supported elements
2010-04-30, by Christian Urban
added eqvt-lemmas for Bex, Ball and Union
2010-04-30, by Christian Urban
NewParser with Parser functionality, but some cheats included since the order of datayupes is wrong.
2010-04-30, by Cezary Kaliszyk
Merged nominal_datatype into NewParser until eqvts
2010-04-30, by Cezary Kaliszyk
more parser/new parser synchronization.
2010-04-30, by Cezary Kaliszyk
Simplify old parser for integration
2010-04-30, by Cezary Kaliszyk
merge
2010-04-30, by Cezary Kaliszyk
Change signature of fv and alpha generation.
2010-04-30, by Cezary Kaliszyk
reorganised eqvt-file (now uses perm_simp already)
2010-04-30, by Christian Urban
qpaper
2010-04-30, by Cezary Kaliszyk
merge
2010-04-29, by Cezary Kaliszyk
New Alpha.
2010-04-29, by Cezary Kaliszyk
Minimal cleaning in LamEx
2010-04-29, by Cezary Kaliszyk
Remove things moved to the isabelle distribution
2010-04-29, by Cezary Kaliszyk
Unify and give only one name to 'setify', 'listify' and 'set'
2010-04-29, by Cezary Kaliszyk
Fixing the definitions in the Parser.
2010-04-29, by Cezary Kaliszyk
Some of the exceptions that the parser should check in TODO.
2010-04-29, by Cezary Kaliszyk
Extracting the fv body function and exporting the terms.
2010-04-29, by Cezary Kaliszyk
Fix for recursive binders.
2010-04-29, by Cezary Kaliszyk
revert 0c9ef14e9ba4
2010-04-29, by Cezary Kaliszyk
Support in positive position and atoms in negative positions.
2010-04-29, by Cezary Kaliszyk
merge
2010-04-29, by Cezary Kaliszyk
Include support of unknown datatypes in new fv
2010-04-29, by Cezary Kaliszyk
merged
2010-04-29, by Christian Urban
added basic functions for constructing supp-terms
2010-04-29, by Christian Urban
quotient paper
2010-04-29, by Cezary Kaliszyk
added missing latex-style file
2010-04-29, by Christian Urban
merged
2010-04-29, by Christian Urban
added stub for quotient paper; call with isabelle make qpaper
2010-04-29, by Christian Urban
Cleaning of Int and FSet Examples
2010-04-28, by Cezary Kaliszyk
use the more general type-class at_base
2010-04-28, by Christian Urban
deleted left-over code
2010-04-28, by Christian Urban
simpliied and moved the remaining lemmas about the atom-function to Nominal2_Base
2010-04-28, by Christian Urban
use sort at_base instead of at
2010-04-28, by Christian Urban
white spaces
2010-04-28, by Christian Urban
avoided repeated dest of dt_info
2010-04-28, by Christian Urban
tuned
2010-04-28, by Christian Urban
factured out common functionality of prefixing the dt-names with a string
2010-04-28, by Christian Urban
closed Datatype_Aux; replaced nth_dtyp by the function used in Perm.thy
2010-04-28, by Christian Urban
added some further problemetic tests
2010-04-27, by Christian Urban
some tuning
2010-04-27, by Christian Urban
moved mk_atom into the library; that meant that concrete atom classes need to be in Nominal2_Base
2010-04-27, by Christian Urban
merged
2010-04-27, by Christian Urban
Rewrote FV code and included the function package.
2010-04-27, by Cezary Kaliszyk
merge
2010-04-27, by Cezary Kaliszyk
Function in Core Haskell
2010-04-27, by Cezary Kaliszyk
one more pass over the paper
2010-04-27, by Christian Urban
more polishing on the paper
2010-04-27, by Christian Urban
merged
2010-04-26, by Christian Urban
some changes to the paper
2010-04-26, by Christian Urban
rewrote eqvts_raw to be a symtab, that can be looked up
2010-04-26, by Christian Urban
merge ???
2010-04-26, by Cezary Kaliszyk
infix for In
2010-04-21, by Cezary Kaliszyk
eliminated command so that all compiles
2010-04-26, by Christian Urban
changed theorem_i to theorem....requires new Isabelle
2010-04-26, by Christian Urban
tuned
2010-04-25, by Christian Urban
tuned and cleaned
2010-04-25, by Christian Urban
tuned and made to compile
2010-04-25, by Christian Urban
added definition of raw-permutations to the new-parser
2010-04-25, by Christian Urban
tuned
2010-04-25, by Christian Urban
slight tuning
2010-04-25, by Christian Urban
added a comment about a function where I am not sure who wrote it.
2010-04-24, by Christian Urban
merged
2010-04-24, by Christian Urban
Minor
2010-04-23, by Cezary Kaliszyk
Minor cleaning of IntEx
2010-04-23, by Cezary Kaliszyk
Further cleaning of proofs in FSet
2010-04-23, by Cezary Kaliszyk
Update term8
2010-04-22, by Cezary Kaliszyk
Converted 'thm' to a lemma.
2010-04-22, by Cezary Kaliszyk
Moved working Fset3 properties to FSet.
2010-04-22, by Cezary Kaliszyk
tuned parser
2010-04-22, by 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
2010-04-22, by Christian Urban
tuned proofs
2010-04-21, by Christian Urban
merged
2010-04-21, by Christian Urban
moved some lemmas into the right places
2010-04-21, by Christian Urban
minor
2010-04-21, by Cezary Kaliszyk
merge
2010-04-21, by Cezary Kaliszyk
append_rsp2 + isarification
2010-04-21, by Cezary Kaliszyk
some small changes
2010-04-21, by Christian Urban
merged
2010-04-21, by Christian Urban
deleted the incomplete proof about pairs of abstractions
2010-04-21, by Christian Urban
added a variant of the induction principle for permutations
2010-04-21, by Christian Urban
merge
2010-04-21, by Cezary Kaliszyk
More about concat
2010-04-21, by Cezary Kaliszyk
merged
2010-04-21, by Christian Urban
incomplete tests
2010-04-21, by Christian Urban
added an improved version of the induction principle for permutations
2010-04-21, by Christian Urban
Working lifting of concat with inline proofs of second level preservation.
2010-04-21, by Cezary Kaliszyk
FSet3 cleaning part2
2010-04-21, by Cezary Kaliszyk
merge
2010-04-21, by Cezary Kaliszyk
Remove the part already in FSet and leave the experiments
2010-04-21, by Cezary Kaliszyk
merged
2010-04-21, by Christian Urban
removed a sorry
2010-04-21, by Christian Urban
renamed Ex1.thy to SingleLet.thy
2010-04-20, by Christian Urban
tuning of the code
2010-04-20, by Christian Urban
Reorder FSet
2010-04-21, by Cezary Kaliszyk
merge
2010-04-21, by Cezary Kaliszyk
lattice properties.
2010-04-21, by Cezary Kaliszyk
All lifted in Term4. Requires new isabelle.
2010-04-20, by Cezary Kaliszyk
fsets are distributive lattices.
2010-04-20, by Cezary Kaliszyk
Fix of comment
2010-04-20, by Cezary Kaliszyk
reordered code
2010-04-20, by Christian Urban
renamed "_empty" and "_append" to "_zero" and "_plus"
2010-04-20, by Christian Urban
removed dead code (nominal cannot deal with argument types of constructors that are functions)
2010-04-20, by Christian Urban
added comment about abstraction in raw permuations
2010-04-20, by Christian Urban
optimised the code of define_raw_perm
2010-04-20, by Christian Urban
deleting function perm_arg in favour of the library function mk_perm
2010-04-19, by Christian Urban
merged
2010-04-19, by Christian Urban
tuned; fleshed out some library functions about permutations; closed Datatype_Aux structure (increases readability)
2010-04-19, by Christian Urban
FSet is a semi-lattice
2010-04-19, by Cezary Kaliszyk
merge
2010-04-19, by Cezary Kaliszyk
Putting FSet in bot typeclass.
2010-04-19, by Cezary Kaliszyk
reorder
2010-04-19, by Cezary Kaliszyk
merged
2010-04-19, by Christian Urban
small updates to the paper; remaining points in PAPER-TODO
2010-04-19, by Christian Urban
sub_list definition and respects
2010-04-19, by Cezary Kaliszyk
Alternate list_eq and equivalence
2010-04-19, by Cezary Kaliszyk
Some new lemmas
2010-04-19, by Cezary Kaliszyk
More cleaning
2010-04-19, by Cezary Kaliszyk
remove more metis
2010-04-19, by Cezary Kaliszyk
more metis cleaning
2010-04-19, by Cezary Kaliszyk
Getting rid of 'metis'.
2010-04-19, by Cezary Kaliszyk
merge
2010-04-19, by Cezary Kaliszyk
Remove 'defer'.
2010-04-19, by Cezary Kaliszyk
merged
2010-04-19, by Christian Urban
tuned proofs
2010-04-19, by Christian Urban
2 more lifted lemmas needed for second representation
2010-04-19, by Cezary Kaliszyk
Accept non-equality eqvt rules in support proofs.
2010-04-19, by Cezary Kaliszyk
merge
2010-04-19, by Cezary Kaliszyk
Locations of files in Parser
2010-04-19, by Cezary Kaliszyk
merge
2010-04-19, by Cezary Kaliszyk
minor FSet3 edits.
2010-04-19, by Cezary Kaliszyk
less
more
|
(0)
-1000
-240
+240
+1000
tip