--- a/src/HOL/Mutabelle/mutabelle.ML Tue Dec 07 16:27:07 2010 +0100
+++ b/src/HOL/Mutabelle/mutabelle.ML Tue Dec 07 17:23:14 2010 +0100
@@ -637,9 +637,9 @@
fun create_spaces entry spacenum =
let
- val diff = spacenum - (size entry)
- in
- if (diff > 0)
+ val diff = spacenum - (size entry)
+ in
+ if (diff > 0)
then implode (replicate diff " ")
else ""
end;
@@ -756,7 +756,7 @@
end;
(*exchange version of function mutqc_thystat*)
-
+
fun mutqc_thystat_exc p mutthy usedthy commutatives iter insts sz qciter filename =
mutqc_thystat 0 p mutthy usedthy commutatives [] iter insts sz qciter filename;
--- a/src/HOL/Quotient_Examples/FSet.thy Tue Dec 07 16:27:07 2010 +0100
+++ b/src/HOL/Quotient_Examples/FSet.thy Tue Dec 07 17:23:14 2010 +0100
@@ -1120,18 +1120,18 @@
have b: "l \<approx> r" by fact
have d: "card_list l = Suc m" by fact
then have "\<exists>a. List.member l a"
- apply(simp)
- apply(drule card_eq_SucD)
- apply(blast)
- done
+ apply(simp)
+ apply(drule card_eq_SucD)
+ apply(blast)
+ done
then obtain a where e: "List.member l a" by auto
then have e': "List.member r a" using list_eq_def [simplified List.member_def [symmetric], of l r] b
- by auto
+ by auto
have f: "card_list (removeAll a l) = m" using e d by (simp)
have g: "removeAll a l \<approx> removeAll a r" using removeAll_rsp b by simp
have "(removeAll a l) \<approx>2 (removeAll a r)" by (rule Suc.hyps[OF f g])
then have h: "(a # removeAll a l) \<approx>2 (a # removeAll a r)" by (rule list_eq2.intros(5))
- have i: "l \<approx>2 (a # removeAll a l)"
+ have i: "l \<approx>2 (a # removeAll a l)"
by (rule list_eq2.intros(3)[OF member_delete_list_eq2[OF e]])
have "l \<approx>2 (a # removeAll a r)" by (rule list_eq2.intros(6)[OF i h])
then show ?case using list_eq2.intros(6)[OF _ member_delete_list_eq2[OF e']] by simp
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Tue Dec 07 16:27:07 2010 +0100
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Tue Dec 07 17:23:14 2010 +0100
@@ -755,7 +755,7 @@
"#!/usr/bin/swipl -q -t main -f\n\n" ^
":- use_module(library('dialect/ciao/aggregates')).\n" ^
":- style_check(-singleton).\n" ^
- ":- style_check(-discontiguous).\n" ^
+ ":- style_check(-discontiguous).\n" ^
":- style_check(-atom).\n\n" ^
"main :- catch(eval, E, (print_message(error, E), fail)), halt.\n" ^
"main :- halt(1).\n"
--- a/src/Pure/pattern.ML Tue Dec 07 16:27:07 2010 +0100
+++ b/src/Pure/pattern.ML Tue Dec 07 17:23:14 2010 +0100
@@ -365,7 +365,7 @@
and cases(binders,env as (iTs,itms),pat,obj) =
let val (ph,pargs) = strip_comb pat
fun rigrig1(iTs,oargs) = fold (mtch binders) (pargs~~oargs) (iTs,itms)
- handle ListPair.UnequalLengths => raise MATCH
+ handle ListPair.UnequalLengths => raise MATCH
fun rigrig2((a:string,Ta),(b,Tb),oargs) =
if a <> b then raise MATCH
else rigrig1(typ_match thy (Ta,Tb) iTs, oargs)