# HG changeset patch
# User wenzelm
# Date 1455363540 -3600
# Node ID 658276428cfc6d08a4388e8c5fe7031ad879697e
# Parent  ffb2743ae0b9f97411de28cf1557352496df942f
isabelle update_cartouches -c -t;

diff -r ffb2743ae0b9 -r 658276428cfc src/Benchmarks/Datatype_Benchmark/IsaFoR.thy
--- a/src/Benchmarks/Datatype_Benchmark/IsaFoR.thy	Sat Feb 13 12:33:55 2016 +0100
+++ b/src/Benchmarks/Datatype_Benchmark/IsaFoR.thy	Sat Feb 13 12:39:00 2016 +0100
@@ -5,7 +5,7 @@
 Benchmark consisting of datatypes defined in IsaFoR.
 *)
 
-section {* Benchmark Consisting of Datatypes Defined in IsaFoR *}
+section \<open>Benchmark Consisting of Datatypes Defined in IsaFoR\<close>
 
 theory IsaFoR
 imports Real
diff -r ffb2743ae0b9 -r 658276428cfc src/Benchmarks/Quickcheck_Benchmark/Find_Unused_Assms_Examples.thy
--- a/src/Benchmarks/Quickcheck_Benchmark/Find_Unused_Assms_Examples.thy	Sat Feb 13 12:33:55 2016 +0100
+++ b/src/Benchmarks/Quickcheck_Benchmark/Find_Unused_Assms_Examples.thy	Sat Feb 13 12:39:00 2016 +0100
@@ -2,7 +2,7 @@
 imports Complex_Main
 begin
 
-section {* Arithmetics *}
+section \<open>Arithmetics\<close>
 
 declare [[quickcheck_finite_types = false]]
 
@@ -10,7 +10,7 @@
 find_unused_assms GCD
 find_unused_assms Real
 
-section {* Set Theory *}
+section \<open>Set Theory\<close>
 
 declare [[quickcheck_finite_types = true]]
 
@@ -19,7 +19,7 @@
 find_unused_assms Set
 find_unused_assms Wellfounded
 
-section {* Datatypes *}
+section \<open>Datatypes\<close>
 
 find_unused_assms List
 find_unused_assms Map
diff -r ffb2743ae0b9 -r 658276428cfc src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Base.thy
--- a/src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Base.thy	Sat Feb 13 12:33:55 2016 +0100
+++ b/src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Base.thy	Sat Feb 13 12:39:00 2016 +0100
@@ -108,7 +108,7 @@
                       | Gets A X   => used evs
                       | Notes A X  => parts {X} \<union> used evs)"
 
-subsection {* Preparations for sets *}
+subsection \<open>Preparations for sets\<close>
 
 fun find_first :: "('a => 'b option) => 'a list => 'b option"
 where
@@ -140,7 +140,7 @@
   [code]: "neg_cps_of_set (set xs) f i = find_first' f xs"
 sorry
 
-setup {*
+setup \<open>
 let
   val Fun = Predicate_Compile_Aux.Fun
   val Input = Predicate_Compile_Aux.Input
@@ -162,9 +162,9 @@
   Core_Data.force_modes_and_compilations @{const_name Set.member}
     [(oi, (of_set, false)), (ii, (member, false))]
 end
-*}
+\<close>
 
-subsection {* Derived equations for analz, parts and synth *}
+subsection \<open>Derived equations for analz, parts and synth\<close>
 
 lemma [code]:
   "analz H = (let
@@ -186,7 +186,7 @@
 
 code_pred [generator_cps] synth' unfolding synth'_def by (rule synth.cases) fastforce+
 
-setup {* Predicate_Compile_Data.ignore_consts [@{const_name analz}, @{const_name knows}] *}
+setup \<open>Predicate_Compile_Data.ignore_consts [@{const_name analz}, @{const_name knows}]\<close>
 declare ListMem_iff[symmetric, code_pred_inline]
 declare [[quickcheck_timing]]
 
diff -r ffb2743ae0b9 -r 658276428cfc src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Guided_Attacker_Example.thy
--- a/src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Guided_Attacker_Example.thy	Sat Feb 13 12:33:55 2016 +0100
+++ b/src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Guided_Attacker_Example.thy	Sat Feb 13 12:39:00 2016 +0100
@@ -55,7 +55,7 @@
 quickcheck[narrowing, size = 7, timeout = 200, expect = no_counterexample]*)
 oops
 
-section {* Proving the counterexample trace for validation *}
+section \<open>Proving the counterexample trace for validation\<close>
 
 lemma
   assumes "A = Alice" "B = Bob" "C = Spy" "NA = 0" "NB = 1"
diff -r ffb2743ae0b9 -r 658276428cfc src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Unguided_Attacker_Example.thy
--- a/src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Unguided_Attacker_Example.thy	Sat Feb 13 12:33:55 2016 +0100
+++ b/src/Benchmarks/Quickcheck_Benchmark/Needham_Schroeder_Unguided_Attacker_Example.thy	Sat Feb 13 12:39:00 2016 +0100
@@ -51,7 +51,7 @@
 (*quickcheck[narrowing, size = 7, timeout = 200, expect = no_counterexample]*)
 oops
 
-section {* Proving the counterexample trace for validation *}
+section \<open>Proving the counterexample trace for validation\<close>
 
 lemma
   assumes "A = Alice" "B = Bob" "C = Spy" "NA = 0" "NB = 1"
diff -r ffb2743ae0b9 -r 658276428cfc src/Benchmarks/Record_Benchmark/Record_Benchmark.thy
--- a/src/Benchmarks/Record_Benchmark/Record_Benchmark.thy	Sat Feb 13 12:33:55 2016 +0100
+++ b/src/Benchmarks/Record_Benchmark/Record_Benchmark.thy	Sat Feb 13 12:39:00 2016 +0100
@@ -2,7 +2,7 @@
     Author:     Norbert Schirmer, DFKI
 *)
 
-section {* Benchmark for large record *}
+section \<open>Benchmark for large record\<close>
 
 theory Record_Benchmark
 imports Main
@@ -355,50 +355,50 @@
   by simp
 
 lemma "(r\<lparr>A255:=x,A253:=y,A255:=z \<rparr>) = r\<lparr>A253:=y,A255:=z\<rparr>"
-  apply (tactic {* simp_tac
-    (put_simpset HOL_basic_ss @{context} addsimprocs [Record.upd_simproc]) 1*})
+  apply (tactic \<open>simp_tac
+    (put_simpset HOL_basic_ss @{context} addsimprocs [Record.upd_simproc]) 1\<close>)
   done
 
 lemma "(\<forall>r. P (A155 r)) \<longrightarrow> (\<forall>x. P x)"
-  apply (tactic {* simp_tac
-    (put_simpset HOL_basic_ss @{context} addsimprocs [Record.split_simproc (K ~1)]) 1*})
+  apply (tactic \<open>simp_tac
+    (put_simpset HOL_basic_ss @{context} addsimprocs [Record.split_simproc (K ~1)]) 1\<close>)
   apply simp
   done
 
 lemma "(\<forall>r. P (A155 r)) \<longrightarrow> (\<forall>x. P x)"
-  apply (tactic {* Record.split_simp_tac @{context} [] (K ~1) 1*})
+  apply (tactic \<open>Record.split_simp_tac @{context} [] (K ~1) 1\<close>)
   apply simp
   done
 
 lemma "(\<exists>r. P (A155 r)) \<longrightarrow> (\<exists>x. P x)"
-  apply (tactic {* simp_tac
-    (put_simpset HOL_basic_ss @{context} addsimprocs [Record.split_simproc (K ~1)]) 1*})
+  apply (tactic \<open>simp_tac
+    (put_simpset HOL_basic_ss @{context} addsimprocs [Record.split_simproc (K ~1)]) 1\<close>)
   apply simp
   done
 
 lemma "(\<exists>r. P (A155 r)) \<longrightarrow> (\<exists>x. P x)"
-  apply (tactic {* Record.split_simp_tac @{context} [] (K ~1) 1*})
+  apply (tactic \<open>Record.split_simp_tac @{context} [] (K ~1) 1\<close>)
   apply simp
   done
 
 lemma "\<And>r. P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
-  apply (tactic {* simp_tac
-    (put_simpset HOL_basic_ss @{context} addsimprocs [Record.split_simproc (K ~1)]) 1*})
+  apply (tactic \<open>simp_tac
+    (put_simpset HOL_basic_ss @{context} addsimprocs [Record.split_simproc (K ~1)]) 1\<close>)
   apply auto
   done
 
 lemma "\<And>r. P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
-  apply (tactic {* Record.split_simp_tac @{context} [] (K ~1) 1*})
+  apply (tactic \<open>Record.split_simp_tac @{context} [] (K ~1) 1\<close>)
   apply auto
   done
 
 lemma "P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
-  apply (tactic {* Record.split_simp_tac @{context} [] (K ~1) 1*})
+  apply (tactic \<open>Record.split_simp_tac @{context} [] (K ~1) 1\<close>)
   apply auto
   done
 
 lemma fixes r shows "P (A155 r) \<Longrightarrow> (\<exists>x. P x)"
-  apply (tactic {* Record.split_simp_tac @{context} [] (K ~1) 1*})
+  apply (tactic \<open>Record.split_simp_tac @{context} [] (K ~1) 1\<close>)
   apply auto
   done
 
@@ -409,15 +409,15 @@
   assume "P (A155 r)"
   then have "\<exists>x. P x"
     apply -
-    apply (tactic {* Record.split_simp_tac @{context} [] (K ~1) 1*})
+    apply (tactic \<open>Record.split_simp_tac @{context} [] (K ~1) 1\<close>)
     apply auto 
     done
 end
 
 
 lemma "\<exists>r. A155 r = x"
-  apply (tactic {*simp_tac
-    (put_simpset HOL_basic_ss @{context} addsimprocs [Record.ex_sel_eq_simproc]) 1*})
+  apply (tactic \<open>simp_tac
+    (put_simpset HOL_basic_ss @{context} addsimprocs [Record.ex_sel_eq_simproc]) 1\<close>)
   done
 
 print_record many_A