| #
91d6f07a |
|
08-Nov-2019 |
wenzelm <none@none> |
tuned comments;
|
| #
5540f58e |
|
12-Oct-2019 |
wenzelm <none@none> |
early setup of proof preprocessing;
|
| #
883ae6cd |
|
11-Oct-2019 |
wenzelm <none@none> |
proper ML names;
|
| #
9a7bc12a |
|
09-Aug-2019 |
wenzelm <none@none> |
clarified ML types;
|
| #
5a9e311d |
|
26-Jul-2019 |
wenzelm <none@none> |
tuned signature;
|
| #
e1232d26 |
|
26-Jul-2019 |
wenzelm <none@none> |
defer rew_proof on unnamed PThm node as open_proof operation: significant performance improvement;
misc tuning and clarification;
|
| #
fe9eef5c |
|
21-Jul-2019 |
wenzelm <none@none> |
global declaration of abstract syntax for proof terms, with qualified names;
clarified modules;
|
| #
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
a7ccdf43 |
|
10-Jan-2018 |
nipkow <none@none> |
ran isabelle update_op on all sources
|
| #
a1264dfa |
|
27-Nov-2017 |
wenzelm <none@none> |
more symbols;
|
| #
9943d69e |
|
27-Nov-2017 |
wenzelm <none@none> |
prefer Input.source (via cartouche);
|
| #
c7cc1919 |
|
26-Nov-2017 |
wenzelm <none@none> |
more symbols;
|
| #
13ddea91 |
|
26-Nov-2014 |
wenzelm <none@none> |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
| #
bf543662 |
|
03-Jun-2010 |
wenzelm <none@none> |
do not open Proofterm, which is very ould style;
|
| #
87ce34be |
|
01-Jun-2010 |
berghofe <none@none> |
Adapted to new format of proof terms containing explicit proofs of class membership.
|
| #
fffcd44c |
|
30-Mar-2010 |
krauss <none@none> |
switched PThm/PAxm etc. to use canonical order of type variables (term variables unchanged)
|
| #
bbc8cf56 |
|
20-Mar-2010 |
wenzelm <none@none> |
renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
|
| #
f5084a96 |
|
16-Nov-2009 |
wenzelm <none@none> |
generalized procs for rewrite_proof: allow skeleton;
fulfill_norm_proof: always normalize result here, no re-normalization after filling;
|
| #
46fafa2e |
|
02-Nov-2009 |
wenzelm <none@none> |
modernized structure Proof_Syntax;
|
| #
a5a5665f |
|
15-Jul-2009 |
wenzelm <none@none> |
more antiquotations;
|
| #
00f1ef6a |
|
02-Apr-2009 |
berghofe <none@none> |
Fixed bug in transformation of congruence rule for ==
(thanks to Andy Schropp for reporting this).
|
| #
8e16d38f |
|
16-Nov-2008 |
wenzelm <none@none> |
clarified Thm.proof_body_of vs. Thm.proof_of;
|
| #
560d2677 |
|
15-Nov-2008 |
wenzelm <none@none> |
ProofSyntax.proof_of_term: removed obsolete disambiguisation table;
adapted PThm;
|
| #
0fb1e6a3 |
|
31-Oct-2008 |
berghofe <none@none> |
Removed argument prf2 in rewrite rules for equal_elim to make them applicable
to eta-contracted proofs.
|
| #
5317e9bf |
|
17-Sep-2008 |
wenzelm <none@none> |
back to dynamic the_context(), because static @{theory} is invalidated if ML environment changes within the same code block;
|
| #
29d095ad |
|
18-Jun-2008 |
wenzelm <none@none> |
more antiquotations;
|
| #
f37947c6 |
|
13-Apr-2008 |
wenzelm <none@none> |
tuned;
|
| #
2ec328e5 |
|
07-Feb-2007 |
berghofe <none@none> |
Fixed bug in mk_AbsP.
|
| #
b5dac97b |
|
04-Dec-2006 |
wenzelm <none@none> |
thm/prf: separate official name vs. additional tags;
|
| #
783590d8 |
|
06-Jun-2006 |
wenzelm <none@none> |
tuned;
|
| #
eee46a1e |
|
02-Mar-2005 |
skalberg <none@none> |
Move towards standard functions.
|
| #
3dffd254 |
|
13-Feb-2005 |
skalberg <none@none> |
Deleted Library.option type.
|
| #
30cc255d |
|
11-Feb-2005 |
berghofe <none@none> |
Fully qualified refl and trans to avoid confusion with theorems
in Lattice_Locales.partial_order.
|
| #
33b1b845 |
|
21-Jun-2004 |
kleing <none@none> |
Merged in license change from Isabelle2004
|
| #
be95e079 |
|
22-Apr-2003 |
berghofe <none@none> |
elim_cong now eta-expands proofs on the fly if required.
|
| #
a09b02b3 |
|
30-Sep-2002 |
berghofe <none@none> |
- additional congruence rules for boolean operators
- additional rewrite rules for exI / exE
|
| #
b6362fe7 |
|
21-Jul-2002 |
berghofe <none@none> |
Rules for rewriting HOL proofs.
|