| #
f5796e6d |
|
14-Feb-2018 |
wenzelm <none@none> |
more symbols;
|
| #
ef344a77 |
|
25-May-2016 |
wenzelm <none@none> |
isabelle update_cartouches -c -t;
|
| #
35f7dccd |
|
23-Feb-2016 |
nipkow <none@none> |
more canonical names
|
| #
548fd697 |
|
13-Mar-2012 |
wenzelm <none@none> |
tuned proofs;
|
| #
ed418196 |
|
28-Dec-2011 |
wenzelm <none@none> |
reverted some changes for set->predicate transition, according to "hg log -u berghofe -r Isabelle2007:Isabelle2008";
tuned proofs;
|
| #
335fd006 |
|
10-Sep-2011 |
wenzelm <none@none> |
misc tuning and clarification;
|
| #
9b4853bb |
|
23-Apr-2011 |
wenzelm <none@none> |
modernized specifications;
|
| #
deac04eb |
|
22-Jul-2010 |
wenzelm <none@none> |
updated some headers;
|
| #
a5f328ca |
|
12-May-2010 |
wenzelm <none@none> |
modernized specifications;
|
| #
baea5702 |
|
01-Mar-2010 |
haftmann <none@none> |
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
|
| #
079cde2d |
|
17-Oct-2009 |
wenzelm <none@none> |
eliminated hard tabulators, guessing at each author's individual tab-width;
tuned headers;
|
| #
26918ebd |
|
07-May-2008 |
berghofe <none@none> |
Manually applied subset_antisym in proof of Compl_fixedpoint, because it is
accidentally applied to predicates as well.
|
| #
02b407a9 |
|
05-Oct-2007 |
nipkow <none@none> |
added lemmas
|
| #
3a22d7a5 |
|
03-Jan-2006 |
paulson <none@none> |
added explicit paths to required theories
|
| #
b66236eb |
|
13-Jul-2005 |
paulson <none@none> |
generlization of some "nat" theorems
|
| #
a7060872 |
|
17-Jun-2005 |
haftmann <none@none> |
migrated theory headers to new format
|
| #
737fdea6 |
|
02-Jun-2005 |
paulson <none@none> |
renamed "constrains" to "safety" to avoid keyword clash
|
| #
db858e97 |
|
02-Aug-2004 |
ballarin <none@none> |
Modifications for trancl_tac (new solver in simplifier).
|
| #
1a1a40cb |
|
26-Jul-2004 |
ballarin <none@none> |
New prover for transitive and reflexive-transitive closure of relations.
- Code in Provers/trancl.ML
- HOL: Simplifier set up to use it as solver
|
| #
5125b879 |
|
15-Aug-2003 |
paulson <none@none> |
A document for UNITY
|
| #
5bb51f23 |
|
08-Feb-2003 |
paulson <none@none> |
converting HOL/UNITY to use unconditional fairness
|
| #
681aa5e4 |
|
05-Feb-2003 |
paulson <none@none> |
more tidying
|
| #
4f0c87b6 |
|
24-Jan-2003 |
paulson <none@none> |
Partial conversion of UNITY to Isar new-style theories
|
| #
543684e4 |
|
01-Dec-2001 |
wenzelm <none@none> |
renamed class "term" to "type" (actually "HOL.type");
|
| #
35842404 |
|
05-Mar-2001 |
paulson <none@none> |
reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp
|