#
ed7a971e |
|
05-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
#
5385dbfa |
|
16-Jan-2018 |
wenzelm <none@none> |
standardized towards new-style formal comments: isabelle update_comments;
|
#
17bc899d |
|
18-Aug-2017 |
wenzelm <none@none> |
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
|
#
66281660 |
|
26-May-2016 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
#
883895af |
|
31-Aug-2015 |
wenzelm <none@none> |
prefer symbols;
|
#
6a7662be |
|
11-Sep-2014 |
blanchet <none@none> |
renamed 'datatype' to 'old_datatype'; 'datatype' is now alias for 'datatype_new'
|
#
aff8c6a4 |
|
12-Feb-2014 |
blanchet <none@none> |
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems * * * more transition of 'xxx_rec' to 'rec_xxx' and same for case * * * compile * * * 'rename_tac's to avoid referring to generated names * * * more robust scripts with 'rename_tac' * * * 'where' -> 'of' * * * 'where' -> 'of' * * * renamed 'xxx_rec' to 'rec_xxx'
|
#
06329277 |
|
13-Aug-2013 |
wenzelm <none@none> |
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
|
#
a51f97fb |
|
28-Nov-2012 |
wenzelm <none@none> |
eliminated slightly odd identifiers;
|
#
e4ce7496 |
|
05-Sep-2012 |
wenzelm <none@none> |
tuned proofs;
|
#
ca569437 |
|
10-Jan-2012 |
berghofe <none@none> |
Removed strange hack introduced in b27e93132603, since equivariance is working again
|
#
deffbbdf |
|
24-Dec-2011 |
haftmann <none@none> |
explicitly spelt out proof of equivariance avoids problem with automation due to type constructor `set`
|
#
ad9e459c |
|
11-Sep-2011 |
nipkow <none@none> |
new fastforce replacing fastsimp - less confusing name
|
#
7a4b6a89 |
|
21-Feb-2011 |
wenzelm <none@none> |
modernized specifications;
|
#
077493ab |
|
08-Sep-2010 |
haftmann <none@none> |
modernized primrec
|
#
2eb87eea |
|
02-Mar-2010 |
haftmann <none@none> |
repaired subscripts broken in d8d7d1b785af
|
#
baea5702 |
|
01-Mar-2010 |
haftmann <none@none> |
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
|
#
f94fe110 |
|
10-Jan-2010 |
berghofe <none@none> |
Adapted to changes in induct method.
|
#
079cde2d |
|
17-Oct-2009 |
wenzelm <none@none> |
eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
|
#
7f1644bf |
|
15-Jul-2009 |
Christian Urban <urbanc@in.tum.de> |
simplified proofs
|
#
2a130c89 |
|
25-Apr-2009 |
Christian Urban <urbanc@in.tum.de> |
deleted thm-attributes "fresh" and "bij" (not used); same features can later be implemented by simpler means
|
#
121e82fb |
|
04-Mar-2009 |
blanchet <none@none> |
Merge.
|
#
6450c0ab |
|
25-Feb-2009 |
berghofe <none@none> |
Added typing and evaluation relations, together with proofs of preservation and progress (i.e. part 2A of the POPLmark challenge).
|
#
1ff366c9 |
|
13-Dec-2008 |
berghofe <none@none> |
Modified nominal_primrec to make it work with local theories, unified syntax with the one used by fun(ction) and new version of primrec command.
|
#
2932189d |
|
22-May-2008 |
urbanc <none@none> |
made the naming of the induction principles consistent: weak_induct is induct and induct is strong_induct
|
#
93be4305 |
|
17-Feb-2008 |
urbanc <none@none> |
updated
|
#
ffa009b0 |
|
11-Jul-2007 |
berghofe <none@none> |
Renamed inductive2 to inductive.
|
#
9ad1fb76 |
|
14-Jun-2007 |
wenzelm <none@none> |
tuned proofs: avoid implicit prems;
|
#
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
|
#
dbad4a37 |
|
28-Mar-2007 |
urbanc <none@none> |
the name for the collection of equivariance lemmas is now eqvts (changed from eqvt) in order to avoid clashes with eqvt-lemmas generated in nominal_inductive
|
#
90ca1a3f |
|
27-Mar-2007 |
urbanc <none@none> |
adapted to nominal_inductive infrastructure
|
#
03f5b25b |
|
12-Mar-2007 |
berghofe <none@none> |
Adapted to new inductive definition package.
|
#
228c94bd |
|
06-Mar-2007 |
urbanc <none@none> |
major update of the nominal package; there is now an infrastructure for equivariance lemmas which eases definitions of nominal functions
|
#
bcb8e017 |
|
27-Nov-2006 |
berghofe <none@none> |
Adapted to new nominal_primrec command.
|
#
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)
|
#
648c3850 |
|
22-Oct-2006 |
berghofe <none@none> |
Adapted to changes in FCBs.
|
#
7517dca8 |
|
11-Sep-2006 |
wenzelm <none@none> |
induct method: renamed 'fixing' to 'arbitrary';
|
#
53020d12 |
|
18-Aug-2006 |
urbanc <none@none> |
adapted using the characteristic equations
|
#
5ac70c1d |
|
17-Aug-2006 |
urbanc <none@none> |
added definition for size and substitution using the recursion combinator
|
#
2f44ec19 |
|
02-Jul-2006 |
urbanc <none@none> |
added more infrastructure for the recursion combinator
|
#
7b184ac8 |
|
28-Apr-2006 |
berghofe <none@none> |
Capitalized theory names.
|
#
6aee2168 |
|
22-Jan-2006 |
urbanc <none@none> |
no essential changes
|
#
a1a9c03c |
|
11-Jan-2006 |
urbanc <none@none> |
cahges to use the new induction-principle (now proved in full glory)
|
#
6fc10121 |
|
11-Jan-2006 |
urbanc <none@none> |
merged the silly lemmas into the eqvt proof of subtype
|
#
ed32531a |
|
10-Jan-2006 |
urbanc <none@none> |
tuned
|
#
5ad8f74d |
|
10-Jan-2006 |
urbanc <none@none> |
tuned
|
#
859ca9b7 |
|
08-Jan-2006 |
urbanc <none@none> |
commented the transitivity and narrowing proof
|
#
acaf67ed |
|
04-Jan-2006 |
urbanc <none@none> |
added more documentation; will now try out a modification of the ok-predicate
|
#
53cde4a6 |
|
16-Dec-2005 |
urbanc <none@none> |
tuned more proofs
|
#
5630fc5e |
|
15-Dec-2005 |
urbanc <none@none> |
there was a small error in the last commit - fixed now
|
#
96ca2c91 |
|
15-Dec-2005 |
urbanc <none@none> |
tuned more proof and added in-file documentation
|
#
191dea92 |
|
15-Dec-2005 |
urbanc <none@none> |
tuned the proof of transitivity/narrowing
|
#
e4fd9007 |
|
15-Dec-2005 |
urbanc <none@none> |
made further tunings
|
#
613a4094 |
|
05-Dec-2005 |
urbanc <none@none> |
transitivity should be now in a reasonable state. But Markus has to have a look at some of the advanced features.
|
#
b874f6d8 |
|
30-Nov-2005 |
urbanc <none@none> |
started to change the transitivity/narrowing case: have trouble with Q=Q.
|
#
e9563eb5 |
|
30-Nov-2005 |
urbanc <none@none> |
changed everything until the interesting transitivity_narrowing proof.
|
#
2f93a07d |
|
27-Nov-2005 |
urbanc <none@none> |
some small tuning
|
#
a2487012 |
|
26-Nov-2005 |
urbanc <none@none> |
added an authors section (please let me know if somebody is left out or unhappy)
|
#
625c0989 |
|
26-Nov-2005 |
urbanc <none@none> |
cleaned up all examples so that they work with the current nominal-setting.
|
#
143a37ca |
|
25-Nov-2005 |
urbanc <none@none> |
added fsub.thy (poplmark challenge) to the examples directory.
|