# HG changeset patch # User Cezary Kaliszyk # Date 1256728926 -3600 # Node ID 8934d21534693f4a0bd1a40bef98a023c660c378 # Parent 89a2ff3f82c779f0e4ca2ca7fd94dfbcded7b5ab Fixed mistake in const generation, will postpone this. diff -r 89a2ff3f82c7 -r 8934d2153469 FSet.thy --- a/FSet.thy Wed Oct 28 10:29:00 2009 +0100 +++ b/FSet.thy Wed Oct 28 12:22:06 2009 +0100 @@ -169,14 +169,14 @@ ML {* val fset_defs = @{thms EMPTY_def IN_def UNION_def card_def INSERT_def fmap_def fold_def} *} -ML {* val consts = map (fst o dest_Const o fst o Logic.dest_equals o concl_of) fset_defs *} +(* ML {* val consts = map (fst o dest_Const o fst o Logic.dest_equals o concl_of) fset_defs *} *) -(* ML {* +ML {* val consts = [@{const_name "Nil"}, @{const_name "Cons"}, @{const_name "membship"}, @{const_name "card1"}, @{const_name "append"}, @{const_name "fold1"}, @{const_name "map"}]; -*} *) +*} ML {* val fset_defs_sym = add_lower_defs @{context} fset_defs *}