Mon, 15 Feb 2010 16:52:32 +0100 |
Cezary Kaliszyk |
merge
|
changeset |
files
|
Mon, 15 Feb 2010 16:51:30 +0100 |
Cezary Kaliszyk |
Fixed the definition of less and finished the missing proof.
|
changeset |
files
|
Mon, 15 Feb 2010 16:50:11 +0100 |
Christian Urban |
further tuning
|
changeset |
files
|
Mon, 15 Feb 2010 16:37:48 +0100 |
Christian Urban |
small tuning
|
changeset |
files
|
Mon, 15 Feb 2010 16:28:07 +0100 |
Christian Urban |
tuned the parsing and testing code in quotient_def.ML; cleaned out old stuff in AbsRepTest.thy
|
changeset |
files
|
Mon, 15 Feb 2010 14:58:03 +0100 |
Cezary Kaliszyk |
der_bname -> derived_bname
|
changeset |
files
|
Mon, 15 Feb 2010 14:51:17 +0100 |
Cezary Kaliszyk |
Names of files.
|
changeset |
files
|
Mon, 15 Feb 2010 14:28:03 +0100 |
Cezary Kaliszyk |
Finished introducing the binding.
|
changeset |
files
|
Mon, 15 Feb 2010 13:40:03 +0100 |
Cezary Kaliszyk |
Synchronize the commands.
|
changeset |
files
|
Mon, 15 Feb 2010 12:23:02 +0100 |
Cezary Kaliszyk |
Passing the binding to quotient_def
|
changeset |
files
|
Mon, 15 Feb 2010 12:15:14 +0100 |
Cezary Kaliszyk |
Added a binding to the parser.
|
changeset |
files
|
Mon, 15 Feb 2010 10:25:17 +0100 |
Cezary Kaliszyk |
Second inline
|
changeset |
files
|
Mon, 15 Feb 2010 10:11:26 +0100 |
Cezary Kaliszyk |
remove one-line wrapper.
|
changeset |
files
|
Fri, 12 Feb 2010 16:27:25 +0100 |
Cezary Kaliszyk |
Undid the read_terms change; now compiles.
|
changeset |
files
|