| Mon, 24 Feb 2020 20:57:29 +0100 |
wenzelm |
more position information for oracles (e.g. "skip_proof" for 'sorry'), requires Proofterm.proofs := 1;
|
file |
diff |
annotate
|
| Sat, 17 Aug 2019 17:21:30 +0200 |
wenzelm |
added ML antiquotation @{oracle_name};
|
file |
diff |
annotate
|
| Sat, 05 Jan 2019 17:24:33 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Sat, 18 Jul 2015 20:54:56 +0200 |
wenzelm |
prefer tactics with explicit context;
|
file |
diff |
annotate
|
| Fri, 06 Mar 2015 15:58:56 +0100 |
wenzelm |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
file |
diff |
annotate
|
| Sat, 22 Nov 2014 14:13:36 +0100 |
wenzelm |
misc tuning and modernization;
|
file |
diff |
annotate
|
| Sun, 02 Nov 2014 18:21:45 +0100 |
wenzelm |
modernized header uniformly as section;
|
file |
diff |
annotate
|
| Mon, 19 Nov 2012 20:23:47 +0100 |
wenzelm |
theorem status about oracles/futures is no longer printed by default;
|
file |
diff |
annotate
|
| Sun, 15 May 2011 17:45:53 +0200 |
wenzelm |
simplified/unified method_setup/attribute_setup;
|
file |
diff |
annotate
|
| Sat, 16 Apr 2011 16:15:37 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Thu, 28 Oct 2010 22:39:59 +0200 |
wenzelm |
moved FOL/ex/Iff_Oracle.thy to HOL/ex where it is more accessible to most readers of isar-ref;
|
file |
diff |
annotate
| base
|