2012-01-24 |
Christian Urban |
tuned make-file
|
file |
diff |
annotate
|
2011-12-29 |
Christian Urban |
separated the two versions of type schemes into two files
|
file |
diff |
annotate
|
2011-12-23 |
Christian Urban |
included Pi theory in tests
|
file |
diff |
annotate
|
2011-12-17 |
Christian Urban |
updated
|
file |
diff |
annotate
|
2011-12-17 |
Christian Urban |
updated in stable branch
Nominal2-Isabelle2011-1
|
file |
diff |
annotate
|
2011-12-17 |
Christian Urban |
updated all examples in stable branch
Nominal2-Isabelle2011-1
|
file |
diff |
annotate
|
2011-11-07 |
Christian Urban |
all examples work again after quotient package has been "de-localised"
|
file |
diff |
annotate
|
2011-11-03 |
Christian Urban |
updated to Isabelle 3 Nov; it includes a hack to work around a bug in the localised version of the quotient package
|
file |
diff |
annotate
|
2011-06-29 |
Christian Urban |
moved Classical and Let temporarily into a section where "sorry" is allowed; this makes all test go through
|
file |
diff |
annotate
|
2011-02-28 |
Christian Urban |
included old test cases for perm_simp into ROOT.ML file
|
file |
diff |
annotate
|
2011-01-06 |
Christian Urban |
moved Weakening up....it does not compile when put at the last position
|
file |
diff |
annotate
|
2011-01-06 |
Christian Urban |
added weakening to the test cases
|
file |
diff |
annotate
|
2010-12-23 |
Christian Urban |
moved all strong_exhaust code to nominal_dt_quot; tuned examples
|
file |
diff |
annotate
|
2010-12-22 |
Christian Urban |
corrected premises of strong exhausts theorems
|
file |
diff |
annotate
|
2010-12-22 |
Christian Urban |
properly exported strong exhaust theorem; cleaned up some examples
|
file |
diff |
annotate
|
2010-11-27 |
Christian Urban |
disabled the Foo examples, because of heavy work
|
file |
diff |
annotate
|
2010-11-24 |
Christian Urban |
added example from the F-ing paper by Rossberg, Russo and Dreyer
|
file |
diff |
annotate
|
2010-11-15 |
Christian Urban |
added a test for the various shallow binders
|
file |
diff |
annotate
|
2010-11-14 |
Christian Urban |
merged Nominal-General directory into Nominal; renamed Abs.thy to Nominal2_Abs.thy
|
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-09-28 |
Christian Urban |
added Foo1 to explore a contrived example
|
file |
diff |
annotate
|
2010-09-22 |
Christian Urban |
fixed
|
file |
diff |
annotate
|
2010-09-22 |
Christian Urban |
made supp proofs more robust by not using the standard induction; renamed some example files
|
file |
diff |
annotate
|
2010-08-29 |
Christian Urban |
renamed NewParser to Nominal2
|
file |
diff |
annotate
|
2010-08-26 |
Christian Urban |
"isabelle make test" makes all major examples....they work up to supp theorems (excluding)
|
file |
diff |
annotate
|
2010-06-23 |
Christian Urban |
merged cezary's changes
|
file |
diff |
annotate
|
2010-05-20 |
Christian Urban |
new fv/fv_bn function (supp breaks now); exported raw perms and raw funs into separate ML-files
|
file |
diff |
annotate
|
2010-05-16 |
Christian Urban |
moved the exporting part into the parser (this is still a hack); re-added CoreHaskell again to the examples - there seems to be a problem with the variable name pat
|
file |
diff |
annotate
|
2010-05-14 |
Christian Urban |
moved old parser and fv into attic
|
file |
diff |
annotate
|
2010-05-13 |
Christian Urban |
added term4 back to the examples
|
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-09 |
Christian Urban |
tuned file names for examples
|
file |
diff |
annotate
|
2010-05-04 |
Cezary Kaliszyk |
"isabelle make" compiles all examples with newparser/newfv/newalpha only.
|
file |
diff |
annotate
|
2010-04-20 |
Christian Urban |
renamed Ex1.thy to SingleLet.thy
|
file |
diff |
annotate
|
2010-04-09 |
Christian Urban |
renamed ExLam to Lambda and completed the proof of the strong ind principle; tuned paper
|
file |
diff |
annotate
|
2010-04-08 |
Christian Urban |
tuned type-schemes example
|
file |
diff |
annotate
|
2010-04-04 |
Christian Urban |
separated general nominal theory into separate folder
|
file |
diff |
annotate
|
2010-04-03 |
Christian Urban |
added README and moved examples into separate directory
|
file |
diff |
annotate
|
2010-03-26 |
Cezary Kaliszyk |
Removed remaining cheats + some cleaning.
|
file |
diff |
annotate
|
2010-03-24 |
Christian Urban |
some tuning; possible fix for strange paper generation
|
file |
diff |
annotate
|
2010-03-23 |
Cezary Kaliszyk |
More modification needed for compilation
|
file |
diff |
annotate
|
2010-03-17 |
Christian Urban |
temporarily disabled tests in Nominal/ROOT
|
file |
diff |
annotate
|
2010-02-25 |
Cezary Kaliszyk |
Split Terms into separate files and add them to tests.
|
file |
diff |
annotate
|
2010-02-25 |
Christian Urban |
added IsaMakefile...but so far included only a test for the parser
|
file |
diff |
annotate
|