src/HOL/Presburger.thy
changeset 56850 13a7bca533a3
parent 54227 63b441f49645
child 57512 cc97b347b301
     1.1 --- a/src/HOL/Presburger.thy	Sun May 04 18:50:42 2014 +0200
     1.2 +++ b/src/HOL/Presburger.thy	Sun May 04 18:53:58 2014 +0200
     1.3 @@ -434,5 +434,9 @@
     1.4  lemma [presburger, algebra]: "m mod (Suc (Suc 0)) = Suc 0 \<longleftrightarrow> \<not> 2 dvd m " by presburger
     1.5  lemma [presburger, algebra]: "m mod 2 = (1::int) \<longleftrightarrow> \<not> 2 dvd m " by presburger
     1.6  
     1.7 +
     1.8 +subsection {* Try0 *}
     1.9 +
    1.10 +ML_file "Tools/try0.ML"
    1.11 +
    1.12  end
    1.13 -