paulson [Tue, 02 Mar 2010 12:59:16 +0000] rev 35509
merged
paulson [Fri, 19 Feb 2010 16:52:11 +0000] rev 35508
merged
paulson [Fri, 19 Feb 2010 15:21:57 +0000] rev 35507
merged
paulson [Fri, 05 Feb 2010 17:19:25 +0000] rev 35506
merged
paulson [Thu, 04 Feb 2010 11:33:54 +0000] rev 35505
merged
paulson [Tue, 02 Feb 2010 09:49:07 +0000] rev 35504
merged
paulson [Tue, 02 Feb 2010 09:48:20 +0000] rev 35503
Correction of a tiny error
krauss [Tue, 02 Mar 2010 17:45:10 +0100] rev 35502
removed obsolete helper theory
haftmann [Tue, 02 Mar 2010 15:39:15 +0100] rev 35501
merged
haftmann [Tue, 02 Mar 2010 15:39:06 +0100] rev 35500
dropped superfluous naming
huffman [Tue, 02 Mar 2010 04:53:18 -0800] rev 35499
UNIV is not a logical constant
huffman [Tue, 02 Mar 2010 04:35:44 -0800] rev 35498
merged
huffman [Tue, 02 Mar 2010 04:31:50 -0800] rev 35497
re-enable bisim code, now in domain_theorems.ML
huffman [Tue, 02 Mar 2010 04:19:06 -0800] rev 35496
add missing rule to case_strict proof script
huffman [Tue, 02 Mar 2010 02:28:45 -0800] rev 35495
remove dead code
huffman [Tue, 02 Mar 2010 00:34:26 -0800] rev 35494
domain package no longer generates copy functions; all proofs use take functions instead
huffman [Mon, 01 Mar 2010 23:54:50 -0800] rev 35493
need to explicitly include REP_convex
huffman [Mon, 01 Mar 2010 19:18:08 -0800] rev 35492
add lemma lub_eq
huffman [Mon, 01 Mar 2010 17:32:23 -0800] rev 35491
add lemmas about ssum_map and sprod_map
huffman [Mon, 01 Mar 2010 16:58:16 -0800] rev 35490
generate take_take rules
huffman [Mon, 01 Mar 2010 16:36:25 -0800] rev 35489
add function define_take_functions
huffman [Mon, 01 Mar 2010 11:15:18 -0800] rev 35488
add missing strictify rule to proof script
huffman [Mon, 01 Mar 2010 10:00:14 -0800] rev 35487
qualify constructor names with type name
huffman [Mon, 01 Mar 2010 09:55:32 -0800] rev 35486
move definition of case combinator to domain_constructors.ML
huffman [Mon, 01 Mar 2010 08:33:49 -0800] rev 35485
remove dependence on Domain_Library
huffman [Mon, 01 Mar 2010 08:14:57 -0800] rev 35484
more uses of function get_vars
huffman [Mon, 01 Mar 2010 07:54:50 -0800] rev 35483
add functions get_vars, get_vars_avoiding
huffman [Mon, 01 Mar 2010 07:35:14 -0800] rev 35482
move proofs of pat_rews to domain_constructors.ML
huffman [Sun, 28 Feb 2010 20:56:28 -0800] rev 35481
add_domain_constructors takes iso_info record as argument
huffman [Sun, 28 Feb 2010 19:39:50 -0800] rev 35480
domain_isomorphism package proves deflation rules for map functions
huffman [Sun, 28 Feb 2010 18:33:57 -0800] rev 35479
store deflation thms for map functions in theory data
huffman [Sun, 28 Feb 2010 18:12:08 -0800] rev 35478
use function list_ccomb
huffman [Sun, 28 Feb 2010 16:11:08 -0800] rev 35477
add function define_const
huffman [Sun, 28 Feb 2010 15:43:09 -0800] rev 35476
fix infix declarations
huffman [Sun, 28 Feb 2010 15:30:44 -0800] rev 35475
move common functions into new file holcf_library.ML
huffman [Sun, 28 Feb 2010 15:09:09 -0800] rev 35474
get rid of incomplete pattern match warnings
huffman [Sun, 28 Feb 2010 14:55:42 -0800] rev 35473
move some powerdomain stuff into a new file
huffman [Sun, 28 Feb 2010 14:05:21 -0800] rev 35472
move case combinator syntax to domain_constructors.ML
huffman [Sun, 28 Feb 2010 12:59:53 -0800] rev 35471
remove redundant code
huffman [Sun, 28 Feb 2010 12:59:21 -0800] rev 35470
use correct syntax name for pattern combinator
huffman [Sun, 28 Feb 2010 09:22:53 -0800] rev 35469
fix output translation for Case syntax
huffman [Sun, 28 Feb 2010 08:55:01 -0800] rev 35468
move definition and syntax of pattern combinators into domain_constructors.ML
huffman [Sat, 27 Feb 2010 21:38:24 -0800] rev 35467
domain_isomorphism function returns iso_info record
huffman [Sat, 27 Feb 2010 20:56:19 -0800] rev 35466
move proofs of match_rews to domain_constructors.ML
huffman [Sat, 27 Feb 2010 20:04:40 -0800] rev 35465
remove dead code
huffman [Sat, 27 Feb 2010 18:45:06 -0800] rev 35464
removed dead code
huffman [Sat, 27 Feb 2010 18:31:52 -0800] rev 35463
register match functions from domain_constructors.ML
huffman [Sat, 27 Feb 2010 18:09:11 -0800] rev 35462
move definition of match combinators to domain_constructors.ML
huffman [Sat, 27 Feb 2010 16:34:13 -0800] rev 35461
move proofs of dis_rews to domain_constructors.ML; change dis_defins to iff-style
huffman [Sat, 27 Feb 2010 15:32:42 -0800] rev 35460
move definition of discriminators to domain_constructors.ML
huffman [Sat, 27 Feb 2010 14:04:46 -0800] rev 35459
move proofs of when_rews intro domain_constructors.ML
huffman [Sat, 27 Feb 2010 10:12:47 -0800] rev 35458
moved proofs of dist_les and dist_eqs to domain_constructors.ML
huffman [Sat, 27 Feb 2010 08:30:11 -0800] rev 35457
move proofs of casedist into domain_constructors.ML
huffman [Fri, 26 Feb 2010 10:54:52 -0800] rev 35456
move proofs of injects and inverts to domain_constructors.ML
huffman [Fri, 26 Feb 2010 10:11:37 -0800] rev 35455
reuse vars_of function
huffman [Fri, 26 Feb 2010 10:06:24 -0800] rev 35454
remove unnecessary stuff from argument to add_constructors function
huffman [Fri, 26 Feb 2010 09:55:56 -0800] rev 35453
reorder sections
huffman [Fri, 26 Feb 2010 09:47:37 -0800] rev 35452
move proof of con_rews into domain_constructor.ML
huffman [Fri, 26 Feb 2010 09:13:29 -0800] rev 35451
don't bother returning con_defs
huffman [Fri, 26 Feb 2010 09:10:50 -0800] rev 35450
move constructor-specific stuff to a separate function