| #
66281660 |
|
26-May-2016 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
| #
06329277 |
|
13-Aug-2013 |
wenzelm <none@none> |
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
|
| #
216c8115 |
|
16-Jan-2011 |
wenzelm <none@none> |
tuned headers;
|
| #
2932189d |
|
22-May-2008 |
urbanc <none@none> |
made the naming of the induction principles consistent: weak_induct is
induct and induct is strong_induct
|
| #
6fb98b8a |
|
28-Jan-2008 |
urbanc <none@none> |
tuned the proof of the substitution lemma
|
| #
84f91899 |
|
04-Jan-2008 |
urbanc <none@none> |
adapted to new inversion rules
|
| #
ffa009b0 |
|
11-Jul-2007 |
berghofe <none@none> |
Renamed inductive2 to inductive.
|
| #
9ad1fb76 |
|
14-Jun-2007 |
wenzelm <none@none> |
tuned proofs: avoid implicit prems;
|
| #
ad772740 |
|
27-Apr-2007 |
urbanc <none@none> |
tuned some proofs in CR and properly included CR_Takahashi
|
| #
f86abfd6 |
|
19-Apr-2007 |
berghofe <none@none> |
nominal_inductive no longer proves equivariance.
|
| #
95572f33 |
|
28-Mar-2007 |
berghofe <none@none> |
- Renamed <predicate>_eqvt to <predicate>.eqvt
- Renamed induct_weak to weak_induct
|
| #
72455713 |
|
28-Mar-2007 |
urbanc <none@none> |
adapted to new nominal_inductive
|
| #
ef19da37 |
|
27-Nov-2006 |
urbanc <none@none> |
adapted function definitions to new syntax
|
| #
20a0be49 |
|
15-Nov-2006 |
urbanc <none@none> |
replaced exists_fresh lemma with a version formulated with obtains;
old lemma is available as exists_fresh' (still needed in apply-scripts)
|
| #
76a64401 |
|
14-Nov-2006 |
wenzelm <none@none> |
inductive2: canonical specification syntax;
ind_cases2: proper treatment of fixed variables;
|
| #
64a3a514 |
|
01-Nov-2006 |
urbanc <none@none> |
changed a misplaced "also" to a "moreover" (caused a loop somehow)
|
| #
42092d70 |
|
01-Nov-2006 |
urbanc <none@none> |
changed to use Lam_Funs
|
| #
e23ef563 |
|
23-Oct-2006 |
urbanc <none@none> |
adapted to Stefan's new inductive package
|
| #
6def9b19 |
|
10-Oct-2006 |
urbanc <none@none> |
made some proof look more like the ones in Barendregt
|
| #
7517dca8 |
|
11-Sep-2006 |
wenzelm <none@none> |
induct method: renamed 'fixing' to 'arbitrary';
|
| #
c9c286d8 |
|
28-Apr-2006 |
berghofe <none@none> |
Capitalized theory names.
|
| #
60a21256 |
|
26-Apr-2006 |
urbanc <none@none> |
isar-keywords.el
- I am not sure what has changed here
nominal.thy
- includes a number of new lemmas (including freshness
and perm_aux things)
nominal_atoms.ML
- no particular changes here
nominal_permeq.ML
- a new version of the decision procedure using
for permutation composition the constant perm_aux
examples
- various adjustments
|
| #
04be3248 |
|
02-Mar-2006 |
urbanc <none@none> |
fixed the bugs itroduced by the previous commit
|
| #
42df7040 |
|
02-Mar-2006 |
urbanc <none@none> |
made some small changes to generate nicer latex-output
|
| #
f07f7ad9 |
|
31-Jan-2006 |
urbanc <none@none> |
- renamed some lemmas (some had names coming from ancient
versions of the nominal work)
- some tuning
- eventually this theory should be renamed to CR
|
| #
c34bd0e9 |
|
24-Jan-2006 |
urbanc <none@none> |
the additional freshness-condition in the one-induction
is not needed anywhere.
|
| #
f8192c41 |
|
11-Jan-2006 |
urbanc <none@none> |
changes to make use of the new induction principle proved by
Stefan horay (hooraayyy)
|
| #
598fad75 |
|
08-Dec-2005 |
urbanc <none@none> |
tuned
|
| #
68011399 |
|
03-Dec-2005 |
urbanc <none@none> |
tuning
|
| #
95424468 |
|
30-Nov-2005 |
urbanc <none@none> |
cleaned up further the proofs (diamond still needs work);
changed "fresh:" to "avoiding:"
|
| #
5ba7fc1b |
|
30-Nov-2005 |
urbanc <none@none> |
modified almost everything for the new nominal_induct
(at the end there are some "normal" inductions which
need a bit more attention)
|
| #
2f93a07d |
|
27-Nov-2005 |
urbanc <none@none> |
some small tuning
|
| #
734bc3dc |
|
07-Nov-2005 |
urbanc <none@none> |
Initial commit.
|