| Thu, 09 Oct 2003 18:13:32 +0200 |
skalberg |
Added support for making constants final, that is, ensuring that no
|
changeset |
files
|
| Wed, 08 Oct 2003 16:02:54 +0200 |
skalberg |
Added axiomatic specifications (ax_specification).
|
changeset |
files
|
| Wed, 08 Oct 2003 15:58:15 +0200 |
paulson |
now accepts DOS and Mac line breaks
|
changeset |
files
|
| Wed, 08 Oct 2003 15:57:41 +0200 |
paulson |
Merging of ex/cla.ML and ex/mesontest.ML to ex/Classical.thy
|
changeset |
files
|
| Fri, 03 Oct 2003 12:36:16 +0200 |
paulson |
added a comment
|
changeset |
files
|
| Thu, 02 Oct 2003 10:57:04 +0200 |
paulson |
removal of junk and improvement of the document
|
changeset |
files
|
| Wed, 01 Oct 2003 11:02:36 +0200 |
berghofe |
Fixed inefficiency in post_definition by adding weak case congruence
|
changeset |
files
|
| Tue, 30 Sep 2003 17:05:50 +0200 |
ballarin |
Removed garbage accidentally left behind in file.
|
changeset |
files
|
| Tue, 30 Sep 2003 15:13:02 +0200 |
ballarin |
Improvements to Isar/Locales: premises generated by "includes" elements
|
changeset |
files
|
| Tue, 30 Sep 2003 15:10:59 +0200 |
ballarin |
Improvements to Isar/Locales: premises generated by "includes" elements
|
changeset |
files
|
| Tue, 30 Sep 2003 15:10:26 +0200 |
ballarin |
Changed order of prems in finprod_cong. Slight speedup.
|
changeset |
files
|
| Tue, 30 Sep 2003 15:09:35 +0200 |
ballarin |
Improvements wrt rule_tac.
|
changeset |
files
|
| Tue, 30 Sep 2003 15:07:38 +0200 |
ballarin |
Improvements to Isar/Locales: premises generated by "includes" elements
|
changeset |
files
|
| Fri, 26 Sep 2003 11:08:18 +0200 |
paulson |
new reference
|
changeset |
files
|
| Fri, 26 Sep 2003 11:04:21 +0200 |
paulson |
tweak
|
changeset |
files
|
| Fri, 26 Sep 2003 10:34:57 +0200 |
paulson |
misc tidying
|
changeset |
files
|
| Fri, 26 Sep 2003 10:34:28 +0200 |
paulson |
Conversion of all main protocols from "Shared" to "Public".
|
changeset |
files
|
| Fri, 26 Sep 2003 10:32:26 +0200 |
paulson |
Tidying of SET's "possibility theorems" (removal of Key_supply_ax)
|
changeset |
files
|
| Wed, 24 Sep 2003 10:44:41 +0200 |
paulson |
new example for the Isar version of the ZF manual
|
changeset |
files
|
| Tue, 23 Sep 2003 20:37:45 +0200 |
skalberg |
Fixed soundness bug.
|
changeset |
files
|
| Tue, 23 Sep 2003 15:49:17 +0200 |
paulson |
conversion of NSP_Bad to Isar script
|
changeset |
files
|
| Tue, 23 Sep 2003 15:44:25 +0200 |
paulson |
case_tac tweak
|
changeset |
files
|
| Tue, 23 Sep 2003 15:42:01 +0200 |
paulson |
some basic new lemmas
|
changeset |
files
|
| Tue, 23 Sep 2003 15:41:33 +0200 |
paulson |
Removal of the Key_supply axiom (affects many possbility proofs) and minor
|
changeset |
files
|
| Tue, 23 Sep 2003 15:40:27 +0200 |
paulson |
new session HOL-SET-Protocol
|
changeset |
files
|
| Mon, 22 Sep 2003 16:19:46 +0200 |
berghofe |
Modified merge_aux to prevent newer names from getting overwritten
|
changeset |
files
|
| Mon, 22 Sep 2003 16:16:03 +0200 |
berghofe |
add_attribute now takes parser as argument.
|
changeset |
files
|
| Mon, 22 Sep 2003 16:14:58 +0200 |
berghofe |
Added "del" attribute for deleting equations.
|
changeset |
files
|