huffman [Thu, 19 Nov 2009 06:01:02 -0800] rev 33780
merged
huffman [Wed, 18 Nov 2009 16:57:58 -0800] rev 33779
remove one_typ and tr_typ; add abs/rep lemmas
huffman [Wed, 18 Nov 2009 16:14:28 -0800] rev 33778
automate definition of rep/abs functions
huffman [Wed, 18 Nov 2009 15:54:47 -0800] rev 33777
get rid of numbers on thy variables
huffman [Wed, 18 Nov 2009 15:51:35 -0800] rev 33776
automate proofs of REP equations
huffman [Wed, 18 Nov 2009 15:01:00 -0800] rev 33775
cleaned up; factored out fixed-point definition code
huffman [Wed, 18 Nov 2009 12:41:43 -0800] rev 33774
automate solution of domain equations
Christian Urban <urbanc@in.tum.de> [Fri, 20 Nov 2009 00:54:20 +0100] rev 33773
removed fixme - quick-and-dirty flag is appropriate
Christian Urban <urbanc@in.tum.de> [Fri, 20 Nov 2009 00:20:32 +0100] rev 33772
use of thm-antiquotation
berghofe [Thu, 19 Nov 2009 16:07:53 +0100] rev 33771
Added new counterexample generator SML_inductive for goals involving
inductive predicates.