| 2011-07-05 |
Christian Urban |
changed bind to binds in specifications; bind will cause trouble with Monad_Syntax
|
file |
diff |
annotate
|
| 2011-06-22 |
Christian Urban |
deleted some dead code
|
file |
diff |
annotate
|
| 2011-06-22 |
Christian Urban |
some rudimentary infrastructure for storing data about nominal datatypes
|
file |
diff |
annotate
|
| 2011-06-16 |
Cezary Kaliszyk |
Fix
|
file |
diff |
annotate
|
| 2011-06-16 |
Christian Urban |
all tests work again
|
file |
diff |
annotate
|
| 2011-06-15 |
Cezary Kaliszyk |
TypeSchemes work with 'default'.
|
file |
diff |
annotate
|
| 2011-06-14 |
Christian Urban |
fixed the problem when giving a complex default-term; the fundef lemmas in Nominal_Base were not general enough
|
file |
diff |
annotate
|
| 2011-06-10 |
Cezary Kaliszyk |
Slightly modify fcb for list1 and put in common place.
|
file |
diff |
annotate
|
| 2011-06-09 |
Cezary Kaliszyk |
abs_res_fcb will be enough to finish the multiple-recursive proof, if we have a working 'default'.
|
file |
diff |
annotate
|
| 2011-06-09 |
Cezary Kaliszyk |
More experiments with 'default'
|
file |
diff |
annotate
|
| 2011-06-08 |
Cezary Kaliszyk |
Issue with 'default'
|
file |
diff |
annotate
|
| 2011-06-08 |
Christian Urban |
merged
|
file |
diff |
annotate
|
| 2011-06-08 |
Christian Urban |
using the option "default" the function package allows one to give an explicit default value
|
file |
diff |
annotate
|
| 2011-06-08 |
Cezary Kaliszyk |
Simpler proof of TypeSchemes/substs
|
file |
diff |
annotate
|
| 2011-06-08 |
Cezary Kaliszyk |
Simplify fcb_res
|
file |
diff |
annotate
|
| 2011-06-08 |
Cezary Kaliszyk |
FCB for res binding and simplified proof of subst for type schemes
|
file |
diff |
annotate
|
| 2011-06-07 |
Christian Urban |
cleaned ups a bit the examples with the invariant framework; exported nominal_function_config datatype into separate structure and file
|
file |
diff |
annotate
|
| 2011-06-02 |
Cezary Kaliszyk |
merge
|
file |
diff |
annotate
|
| 2011-06-02 |
Cezary Kaliszyk |
Remove SMT
|
file |
diff |
annotate
|
| 2011-06-01 |
Christian Urban |
hopefully final fix for ho-functions
|
file |
diff |
annotate
|
| 2011-06-01 |
Cezary Kaliszyk |
proved subst for All constructor in type schemes.
|
file |
diff |
annotate
|
| 2011-05-25 |
Christian Urban |
added eq_iff and distinct lemmas of nominal datatypes to the simplifier
|
file |
diff |
annotate
|
| 2011-02-19 |
Cezary Kaliszyk |
typeschemes/subst
|
file |
diff |
annotate
|
| 2011-02-17 |
Cezary Kaliszyk |
further experiments with typeschemes subst
|
file |
diff |
annotate
|
| 2011-02-07 |
Christian Urban |
cleaned up the experiments so that the tests go through
|
file |
diff |
annotate
|
| 2011-01-31 |
Cezary Kaliszyk |
Experiments with substitution on set+
|
file |
diff |
annotate
|
| 2011-01-30 |
Cezary Kaliszyk |
Showing that the binders difference is fresh for the left side solves the goal for 'set'.
|
file |
diff |
annotate
|
| 2011-01-29 |
Cezary Kaliszyk |
Experiments with functions
|
file |
diff |
annotate
|
| 2011-01-27 |
Christian Urban |
some experiments
|
file |
diff |
annotate
|
| 2011-01-25 |
Christian Urban |
made eqvt-proof explicit in the function definitions
|
file |
diff |
annotate
|
| 2011-01-18 |
Christian Urban |
some tryes about substitution over type-schemes
|
file |
diff |
annotate
|
| 2010-12-31 |
Christian Urban |
changed res keyword to set+ for restrictions; comment by a referee
|
file |
diff |
annotate
|
| 2010-12-28 |
Christian Urban |
automated all strong induction lemmas
|
file |
diff |
annotate
|
| 2010-12-22 |
Christian Urban |
tuned examples
|
file |
diff |
annotate
|
| 2010-12-22 |
Christian Urban |
properly exported strong exhaust theorem; cleaned up some examples
|
file |
diff |
annotate
|
| 2010-12-16 |
Christian Urban |
simple cases for strong inducts done; infrastructure for the difficult ones is there
|
file |
diff |
annotate
|
| 2010-11-14 |
Christian Urban |
moved rest of the lemmas from Nominal2_FSet to the TypeScheme example
|
file |
diff |
annotate
|
| 2010-11-06 |
Christian Urban |
added a test about subtyping; disabled two tests, because of problem with function package
|
file |
diff |
annotate
|
| 2010-10-14 |
Christian Urban |
major reorganisation of fset (renamed fset_to_set to fset, changed the definition of list_eq and fcard_raw)
|
file |
diff |
annotate
|
| 2010-09-28 |
Christian Urban |
added Foo1 to explore a contrived example
|
file |
diff |
annotate
|
| 2010-09-27 |
Christian Urban |
added postprocessed fresh-lemmas for constructors
|
file |
diff |
annotate
|
| 2010-09-25 |
Christian Urban |
cleaned up two examples
|
file |
diff |
annotate
|
| 2010-09-20 |
Christian Urban |
introduced a general procedure for structural inductions; simplified reflexivity proof
|
file |
diff |
annotate
|
| 2010-09-03 |
Christian Urban |
moved a proof to Abs
|
file |
diff |
annotate
|
| 2010-08-29 |
Christian Urban |
renamed NewParser to Nominal2
|
file |
diff |
annotate
|
| 2010-08-28 |
Christian Urban |
added fs-instance proofs
|
file |
diff |
annotate
|
| 2010-08-28 |
Christian Urban |
added proofs for fsupp properties
|
file |
diff |
annotate
|
| 2010-08-25 |
Christian Urban |
cleaned up (almost completely) the examples
|
file |
diff |
annotate
|
| 2010-08-25 |
Christian Urban |
automatic lifting
|
file |
diff |
annotate
|
| 2010-08-21 |
Christian Urban |
changed parser so that the binding mode is indicated as "bind (list)", "bind (set)" or "bind (res)"; if only "bind" is given, then bind (list) is assumed as default
|
file |
diff |
annotate
|
| 2010-06-27 |
Christian Urban |
fixed according to changes in quotient
|
file |
diff |
annotate
|
| 2010-06-02 |
Christian Urban |
fixed problem with bn_info
|
file |
diff |
annotate
|
| 2010-05-25 |
Cezary Kaliszyk |
Substitution Lemma for TypeSchemes.
|
file |
diff |
annotate
|
| 2010-05-25 |
Cezary Kaliszyk |
Simplified the proof
|
file |
diff |
annotate
|
| 2010-05-25 |
Cezary Kaliszyk |
A lemma about substitution in TypeSchemes.
|
file |
diff |
annotate
|
| 2010-05-12 |
Christian Urban |
fixed the examples for the new eqvt-procedure....temporarily disabled Manual/Term4.thy
|
file |
diff |
annotate
|
| 2010-05-11 |
Cezary Kaliszyk |
Include raw permutation definitions in eqvt
|
file |
diff |
annotate
|
| 2010-05-11 |
Cezary Kaliszyk |
Declare alpha_gen_eqvt as eqvt and change the proofs that used 'eqvts[symmetric]'
|
file |
diff |
annotate
|
| 2010-05-09 |
Christian Urban |
cleaned up a bit the examples; added equivariance to all examples
|
file |
diff |
annotate
|
| 2010-05-04 |
Cezary Kaliszyk |
Move TypeSchemes to NewParser
|
file |
diff |
annotate
|