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
```