src/HOL/SMT_Examples/SMT_Examples.thy
changeset 66740 ece9435ca78e
parent 66298 5ff9fe3fee66
child 66758 9312ce5a938d
     1.1 --- a/src/HOL/SMT_Examples/SMT_Examples.thy	Sun Oct 01 15:17:31 2017 +0200
     1.2 +++ b/src/HOL/SMT_Examples/SMT_Examples.thy	Sun Oct 01 15:17:43 2017 +0200
     1.3 @@ -35,7 +35,8 @@
     1.4  axiomatization symm_f :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where
     1.5    symm_f: "symm_f x y = symm_f y x"
     1.6  
     1.7 -lemma "a = a \<and> symm_f a b = symm_f b a" by (smt symm_f)
     1.8 +lemma "a = a \<and> symm_f a b = symm_f b a"
     1.9 +  by (smt symm_f)
    1.10  
    1.11  (*
    1.12  Taken from ~~/src/HOL/ex/SAT_Examples.thy.
    1.13 @@ -474,11 +475,14 @@
    1.14  
    1.15  section \<open>Monomorphization examples\<close>
    1.16  
    1.17 -definition Pred :: "'a \<Rightarrow> bool" where "Pred x = True"
    1.18 +definition Pred :: "'a \<Rightarrow> bool" where
    1.19 +  "Pred x = True"
    1.20  
    1.21 -lemma poly_Pred: "Pred x \<and> (Pred [x] \<or> \<not> Pred [x])" by (simp add: Pred_def)
    1.22 +lemma poly_Pred: "Pred x \<and> (Pred [x] \<or> \<not> Pred [x])"
    1.23 +  by (simp add: Pred_def)
    1.24  
    1.25 -lemma "Pred (1::int)" by (smt poly_Pred)
    1.26 +lemma "Pred (1::int)"
    1.27 +  by (smt poly_Pred)
    1.28  
    1.29  axiomatization g :: "'a \<Rightarrow> nat"
    1.30  axiomatization where