Mon, 15 Feb 2010 13:40:03 +0100 Cezary Kaliszyk Synchronize the commands.
Mon, 15 Feb 2010 12:23:02 +0100 Cezary Kaliszyk Passing the binding to quotient_def
Mon, 15 Feb 2010 12:15:14 +0100 Cezary Kaliszyk Added a binding to the parser.
Mon, 15 Feb 2010 10:25:17 +0100 Cezary Kaliszyk Second inline
Mon, 15 Feb 2010 10:11:26 +0100 Cezary Kaliszyk remove one-line wrapper.
Fri, 12 Feb 2010 16:27:25 +0100 Cezary Kaliszyk Undid the read_terms change; now compiles.
Fri, 12 Feb 2010 16:06:09 +0100 Cezary Kaliszyk merge
Fri, 12 Feb 2010 16:04:10 +0100 Cezary Kaliszyk renamed 'as' to 'is' everywhere.
Fri, 12 Feb 2010 15:50:43 +0100 Cezary Kaliszyk "is" defined as the keyword
Fri, 12 Feb 2010 15:06:20 +0100 Christian Urban moved "strange" lemma to quotient_tacs; marked a number of lemmas as unused; tuned
Fri, 12 Feb 2010 12:06:09 +0100 Cezary Kaliszyk The lattice instantiations are gone from Isabelle/Main, so
Thu, 11 Feb 2010 17:58:06 +0100 Cezary Kaliszyk the lam/bla example.
(0) -1000 -300 -100 -12 +12 +100 +300 +1000 tip