Tue, 05 Oct 2010 17:32:02 -0700 move lemmas to Deflation.thy
Brian Huffman <brianh@cs.pdx.edu> [Tue, 05 Oct 2010 17:32:02 -0700] rev 39971
move lemmas to Deflation.thy
Tue, 05 Oct 2010 17:07:57 -0700 simplify proofs of powerdomain inequalities
Brian Huffman <brianh@cs.pdx.edu> [Tue, 05 Oct 2010 17:07:57 -0700] rev 39970
simplify proofs of powerdomain inequalities
Mon, 04 Oct 2010 06:58:37 -0700 new lemmas about lub
huffman [Mon, 04 Oct 2010 06:58:37 -0700] rev 39969
new lemmas about lub
Mon, 04 Oct 2010 06:45:57 -0700 define is_ub predicate using bounded quantifier
huffman [Mon, 04 Oct 2010 06:45:57 -0700] rev 39968
define is_ub predicate using bounded quantifier
Sat, 02 Oct 2010 17:50:33 -0700 minimize theory imports
huffman [Sat, 02 Oct 2010 17:50:33 -0700] rev 39967
minimize theory imports
Fri, 01 Oct 2010 07:40:57 -0700 added lemmas to List_Cpo.thy
huffman [Fri, 01 Oct 2010 07:40:57 -0700] rev 39966
added lemmas to List_Cpo.thy
Thu, 30 Sep 2010 19:42:12 -0700 new_domain emits proper error message when a constructor argument type does not have sort 'rep'
huffman [Thu, 30 Sep 2010 19:42:12 -0700] rev 39965
new_domain emits proper error message when a constructor argument type does not have sort 'rep'
Wed, 06 Oct 2010 17:56:41 +0200 move code from "Metis_Tactics" to "Metis_Reconstruct"
blanchet [Wed, 06 Oct 2010 17:56:41 +0200] rev 39964
move code from "Metis_Tactics" to "Metis_Reconstruct"
Wed, 06 Oct 2010 17:44:21 +0200 merged
blanchet [Wed, 06 Oct 2010 17:44:21 +0200] rev 39963
merged
Wed, 06 Oct 2010 17:44:07 +0200 qualify "Meson." and "Metis." constants so that the ML files can be reloaded later (e.g. for testing/development)
blanchet [Wed, 06 Oct 2010 17:44:07 +0200] rev 39962
qualify "Meson." and "Metis." constants so that the ML files can be reloaded later (e.g. for testing/development)
(0) -30000 -10000 -3000 -1000 -300 -100 -10 +10 +100 +300 +1000 +3000 +10000 +30000 tip