| #
79eeedc3 |
|
06-Aug-2019 |
wenzelm <none@none> |
more careful treatment of implicit context;
|
| #
e60cf64d |
|
06-Jan-2019 |
wenzelm <none@none> |
isabelle update -u path_cartouches;
|
| #
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
455aefc7 |
|
24-Jun-2018 |
wenzelm <none@none> |
simplified ZF theory names (in contrast to 6a0801279f4c): session-qualification already achieves disjointness;
--HG--
rename : src/ZF/Datatype_ZF.thy => src/ZF/Datatype.thy
rename : src/ZF/Inductive_ZF.thy => src/ZF/Inductive.thy
rename : src/ZF/Int_ZF.thy => src/ZF/Int.thy
rename : src/ZF/IntDiv_ZF.thy => src/ZF/IntDiv.thy
rename : src/ZF/List_ZF.thy => src/ZF/List.thy
rename : src/ZF/Nat_ZF.thy => src/ZF/Nat.thy
|
| #
e7a16ceb |
|
07-Oct-2007 |
wenzelm <none@none> |
modernized specifications;
removed legacy ML bindings;
|
| #
d6f3bba4 |
|
19-Jun-2007 |
wenzelm <none@none> |
BalancedTree;
|
| #
7e06db14 |
|
26-Apr-2007 |
wenzelm <none@none> |
removed lagacy ML files;
|
| #
a7060872 |
|
17-Jun-2005 |
haftmann <none@none> |
migrated theory headers to new format
|
| #
82107132 |
|
09-Jul-2002 |
paulson <none@none> |
better document preparation
|
| #
0ec718f6 |
|
14-Nov-2001 |
wenzelm <none@none> |
adapted primrec/datatype to Isar;
|
| #
f1872714 |
|
13-Nov-2001 |
wenzelm <none@none> |
rearranged inductive package for Isar;
|
| #
0649249a |
|
07-Jan-1999 |
paulson <none@none> |
ZF: the natural numbers as a datatype
|
| #
b5894316 |
|
28-Dec-1998 |
paulson <none@none> |
new inductive, datatype and primrec packages, etc.
|
| #
d23d75d9 |
|
02-Apr-1997 |
paulson <none@none> |
Now a non-trivial theory so that require_thy can find it
|
| #
50b5b460 |
|
19-Dec-1994 |
lcp <none@none> |
removed quotes around "Inductive"
|
| #
37eef679 |
|
24-Aug-1994 |
lcp <none@none> |
ZF/Inductive.thy,.ML: renamed from "inductive" to allow re-building without
the keyword "inductive" making the theory file fail
ZF/Makefile: now has Inductive.thy,.ML
ZF/Datatype,Finite,Zorn: depend upon Inductive
ZF/intr_elim: now checks that the inductive name does not clash with
existing theory names
ZF/ind_section: deleted things replicated in Pure/section_utils.ML
ZF/ROOT: now loads Pure/section_utils
|
| #
9df696ad |
|
11-Aug-1994 |
lcp <none@none> |
installation of new inductive/datatype sections
|
| #
5c777ea1 |
|
16-Nov-1993 |
clasohm <none@none> |
made pseudo theories for all ML files;
documented dependencies between all thy and ML files
|