# HG changeset patch # User haftmann # Date 1125900875 -7200 # Node ID 0ab67cb765dafc4e05172de5bb9a882a65122531 # Parent 526ff7cfd6ea67b4b1f219b9fc9d7971083dd02e introduced binding priority 1 for linear combinators etc. diff -r 526ff7cfd6ea -r 0ab67cb765da src/HOL/Tools/record_package.ML --- a/src/HOL/Tools/record_package.ML Sat Sep 03 22:27:06 2005 +0200 +++ b/src/HOL/Tools/record_package.ML Mon Sep 05 08:14:35 2005 +0200 @@ -1178,8 +1178,8 @@ val simprocs = if has_rec goal then [record_split_simproc P] else []; - in st |> (EVERY split_frees_tacs) - THEN (Simplifier.full_simp_tac (simpset addsimps thms addsimprocs simprocs) i) + in st |> ((EVERY split_frees_tacs) + THEN (Simplifier.full_simp_tac (simpset addsimps thms addsimprocs simprocs) i)) end handle Empty => Seq.empty; end; diff -r 526ff7cfd6ea -r 0ab67cb765da src/Provers/blast.ML --- a/src/Provers/blast.ML Sat Sep 03 22:27:06 2005 +0200 +++ b/src/Provers/blast.ML Mon Sep 05 08:14:35 2005 +0200 @@ -455,7 +455,7 @@ (*Like dup_elim, but puts the duplicated major premise FIRST*) -fun rev_dup_elim th = th RSN (2, revcut_rl) |> assumption 2 |> Seq.hd; +fun rev_dup_elim th = (th RSN (2, revcut_rl)) |> assumption 2 |> Seq.hd; (*Rotate the assumptions in all new subgoals for the LIFO discipline*) diff -r 526ff7cfd6ea -r 0ab67cb765da src/Provers/classical.ML --- a/src/Provers/classical.ML Sat Sep 03 22:27:06 2005 +0200 +++ b/src/Provers/classical.ML Mon Sep 05 08:14:35 2005 +0200 @@ -212,7 +212,7 @@ fun dup_elim th = (case try (fn () => rule_by_tactic (TRYALL (etac revcut_rl)) - (th RSN (2, revcut_rl) |> assumption 2 |> Seq.hd)) () of + ((th RSN (2, revcut_rl)) |> assumption 2 |> Seq.hd)) () of SOME th' => th' | _ => error ("Bad format for elimination rule\n" ^ string_of_thm th)); diff -r 526ff7cfd6ea -r 0ab67cb765da src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Sat Sep 03 22:27:06 2005 +0200 +++ b/src/Pure/Isar/locale.ML Mon Sep 05 08:14:35 2005 +0200 @@ -1896,10 +1896,10 @@ Tactic.compose_tac (false, Drule.conj_intr_list (map (Thm.assume o cert) norm_ts), 0) 1)); val conjuncts = - Drule.equal_elim_rule1 OF [Thm.symmetric body_eq, - Tactic.rewrite_rule [pred_def] (Thm.assume (cert statement))] + (Drule.equal_elim_rule1 OF [Thm.symmetric body_eq, + Tactic.rewrite_rule [pred_def] (Thm.assume (cert statement))]) |> Drule.conj_elim_precise (length ts); - val axioms = (ts ~~ conjuncts) |> map (fn (t, ax) => + val axioms = ts ~~ conjuncts |> map (fn (t, ax) => Tactic.prove_plain defs_thy [] [] t (fn _ => Tactic.rewrite_goals_tac defs THEN Tactic.compose_tac (false, ax, 0) 1)); diff -r 526ff7cfd6ea -r 0ab67cb765da src/Pure/library.ML --- a/src/Pure/library.ML Sat Sep 03 22:27:06 2005 +0200 +++ b/src/Pure/library.ML Mon Sep 05 08:14:35 2005 +0200 @@ -8,14 +8,13 @@ tables, balanced trees, orders, current directory, misc. *) -infix |> |-> ||> ||>> |>> |>>> #> #-> ~~ \ \\ ins ins_string ins_int - orf andf prefix upto downto mem mem_int mem_string union union_int - union_string inter inter_int inter_string subset subset_int - subset_string; +infix 1 |> |-> ||> ||>> |>> |>>> #> #->; +infix 2 ?; +infix 3 o oo ooo oooo; -infix 2 ?; - -infix 3 oo ooo oooo; +infix 4 ~~ upto downto; +infix orf andf prefix \ \\ ins ins_string ins_int mem mem_int mem_string union union_int + union_string inter inter_int inter_string subset subset_int subset_string; signature BASIC_LIBRARY = sig