--- a/src/FOL/FOL.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/FOL/FOL.thy Sat Feb 19 08:39:05 2011 +0100
@@ -18,7 +18,7 @@
subsection {* The classical axiom *}
-axioms
+axiomatization where
classical: "(~P ==> P) ==> P"
--- a/src/FOL/IFOL.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/FOL/IFOL.thy Sat Feb 19 08:39:05 2011 +0100
@@ -88,42 +88,39 @@
finalconsts
False All Ex eq conj disj imp
-axioms
-
+axiomatization where
(* Equality *)
-
- refl: "a=a"
+ refl: "a=a" and
subst: "a=b \<Longrightarrow> P(a) \<Longrightarrow> P(b)"
+
+axiomatization where
(* Propositional logic *)
-
- conjI: "[| P; Q |] ==> P&Q"
- conjunct1: "P&Q ==> P"
- conjunct2: "P&Q ==> Q"
+ conjI: "[| P; Q |] ==> P&Q" and
+ conjunct1: "P&Q ==> P" and
+ conjunct2: "P&Q ==> Q" and
- disjI1: "P ==> P|Q"
- disjI2: "Q ==> P|Q"
- disjE: "[| P|Q; P ==> R; Q ==> R |] ==> R"
+ disjI1: "P ==> P|Q" and
+ disjI2: "Q ==> P|Q" and
+ disjE: "[| P|Q; P ==> R; Q ==> R |] ==> R" and
- impI: "(P ==> Q) ==> P-->Q"
- mp: "[| P-->Q; P |] ==> Q"
+ impI: "(P ==> Q) ==> P-->Q" and
+ mp: "[| P-->Q; P |] ==> Q" and
FalseE: "False ==> P"
+axiomatization where
(* Quantifiers *)
+ allI: "(!!x. P(x)) ==> (ALL x. P(x))" and
+ spec: "(ALL x. P(x)) ==> P(x)" and
- allI: "(!!x. P(x)) ==> (ALL x. P(x))"
- spec: "(ALL x. P(x)) ==> P(x)"
-
- exI: "P(x) ==> (EX x. P(x))"
+ exI: "P(x) ==> (EX x. P(x))" and
exE: "[| EX x. P(x); !!x. P(x) ==> R |] ==> R"
-axioms
-
+axiomatization where
(* Reflection, admissible *)
-
- eq_reflection: "(x=y) ==> (x==y)"
+ eq_reflection: "(x=y) ==> (x==y)" and
iff_reflection: "(P<->Q) ==> (P==Q)"
--- a/src/FOL/ex/If.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/FOL/ex/If.thy Sat Feb 19 08:39:05 2011 +0100
@@ -1,4 +1,4 @@
-(* Title: FOL/ex/If.ML
+(* Title: FOL/ex/If.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
*)
--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy Sat Feb 19 08:39:05 2011 +0100
@@ -13,10 +13,10 @@
zero :: int ("0")
minus :: "int => int" ("- _")
-axioms
- int_assoc: "(x + y::int) + z = x + (y + z)"
- int_zero: "0 + x = x"
- int_minus: "(-x) + x = 0"
+axiomatization where
+ int_assoc: "(x + y::int) + z = x + (y + z)" and
+ int_zero: "0 + x = x" and
+ int_minus: "(-x) + x = 0" and
int_minus2: "-(-x) = x"
section {* Inference of parameter types *}
@@ -527,13 +527,12 @@
end
-consts
- gle :: "'a => 'a => o" gless :: "'a => 'a => o"
- gle' :: "'a => 'a => o" gless' :: "'a => 'a => o"
-
-axioms
- grefl: "gle(x, x)" gless_def: "gless(x, y) <-> gle(x, y) & x ~= y"
- grefl': "gle'(x, x)" gless'_def: "gless'(x, y) <-> gle'(x, y) & x ~= y"
+axiomatization
+ gle :: "'a => 'a => o" and gless :: "'a => 'a => o" and
+ gle' :: "'a => 'a => o" and gless' :: "'a => 'a => o"
+where
+ grefl: "gle(x, x)" and gless_def: "gless(x, y) <-> gle(x, y) & x ~= y" and
+ grefl': "gle'(x, x)" and gless'_def: "gless'(x, y) <-> gle'(x, y) & x ~= y"
text {* Setup *}
--- a/src/FOL/ex/Nat.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/FOL/ex/Nat.thy Sat Feb 19 08:39:05 2011 +0100
@@ -12,21 +12,19 @@
typedecl nat
arities nat :: "term"
-consts
- Zero :: nat ("0")
- Suc :: "nat => nat"
+axiomatization
+ Zero :: nat ("0") and
+ Suc :: "nat => nat" and
rec :: "[nat, 'a, [nat, 'a] => 'a] => 'a"
- add :: "[nat, nat] => nat" (infixl "+" 60)
+where
+ induct: "[| P(0); !!x. P(x) ==> P(Suc(x)) |] ==> P(n)" and
+ Suc_inject: "Suc(m)=Suc(n) ==> m=n" and
+ Suc_neq_0: "Suc(m)=0 ==> R" and
+ rec_0: "rec(0,a,f) = a" and
+ rec_Suc: "rec(Suc(m), a, f) = f(m, rec(m,a,f))"
-axioms
- induct: "[| P(0); !!x. P(x) ==> P(Suc(x)) |] ==> P(n)"
- Suc_inject: "Suc(m)=Suc(n) ==> m=n"
- Suc_neq_0: "Suc(m)=0 ==> R"
- rec_0: "rec(0,a,f) = a"
- rec_Suc: "rec(Suc(m), a, f) = f(m, rec(m,a,f))"
-
-defs
- add_def: "m+n == rec(m, n, %x y. Suc(y))"
+definition add :: "[nat, nat] => nat" (infixl "+" 60)
+ where "m + n == rec(m, n, %x y. Suc(y))"
subsection {* Proofs about the natural numbers *}
--- a/src/FOL/ex/Prolog.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/FOL/ex/Prolog.thy Sat Feb 19 08:39:05 2011 +0100
@@ -11,15 +11,16 @@
typedecl 'a list
arities list :: ("term") "term"
-consts
- Nil :: "'a list"
- Cons :: "['a, 'a list]=> 'a list" (infixr ":" 60)
- app :: "['a list, 'a list, 'a list] => o"
+
+axiomatization
+ Nil :: "'a list" and
+ Cons :: "['a, 'a list]=> 'a list" (infixr ":" 60) and
+ app :: "['a list, 'a list, 'a list] => o" and
rev :: "['a list, 'a list] => o"
-axioms
- appNil: "app(Nil,ys,ys)"
- appCons: "app(xs,ys,zs) ==> app(x:xs, ys, x:zs)"
- revNil: "rev(Nil,Nil)"
+where
+ appNil: "app(Nil,ys,ys)" and
+ appCons: "app(xs,ys,zs) ==> app(x:xs, ys, x:zs)" and
+ revNil: "rev(Nil,Nil)" and
revCons: "[| rev(xs,ys); app(ys, x:Nil, zs) |] ==> rev(x:xs, zs)"
schematic_lemma "app(a:b:c:Nil, d:e:Nil, ?x)"
--- a/src/FOL/ex/Quantifiers_Cla.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/FOL/ex/Quantifiers_Cla.thy Sat Feb 19 08:39:05 2011 +0100
@@ -1,4 +1,4 @@
-(* Title: FOL/ex/Quantifiers_Int.thy
+(* Title: FOL/ex/Quantifiers_Cla.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
*)
--- a/src/FOLP/FOLP.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/FOLP/FOLP.thy Sat Feb 19 08:39:05 2011 +0100
@@ -11,10 +11,8 @@
("classical.ML") ("simp.ML") ("simpdata.ML")
begin
-consts
- cla :: "[p=>p]=>p"
-axioms
- classical: "(!!x. x:~P ==> f(x):P) ==> cla(f):P"
+axiomatization cla :: "[p=>p]=>p"
+ where classical: "(!!x. x:~P ==> f(x):P) ==> cla(f):P"
(*** Classical introduction rules for | and EX ***)
--- a/src/FOLP/ex/Foundation.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/FOLP/ex/Foundation.thy Sat Feb 19 08:39:05 2011 +0100
@@ -1,4 +1,4 @@
-(* Title: FOLP/ex/Foundation.ML
+(* Title: FOLP/ex/Foundation.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1991 University of Cambridge
*)
--- a/src/FOLP/ex/Nat.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/FOLP/ex/Nat.thy Sat Feb 19 08:39:05 2011 +0100
@@ -1,4 +1,4 @@
-(* Title: FOLP/ex/nat.thy
+(* Title: FOLP/ex/Nat.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
*)
--- a/src/HOL/Auth/Guard/Analz.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/HOL/Auth/Guard/Analz.thy Sat Feb 19 08:39:05 2011 +0100
@@ -1,13 +1,7 @@
-(******************************************************************************
-date: december 2001
-author: Frederic Blanqui
-email: blanqui@lri.fr
-webpage: http://www.lri.fr/~blanqui/
-
-University of Cambridge, Computer Laboratory
-William Gates Building, JJ Thomson Avenue
-Cambridge CB3 0FD, United Kingdom
-******************************************************************************)
+(* Title: HOL/Auth/Guard/Analz.thy
+ Author: Frederic Blanqui, University of Cambridge Computer Laboratory
+ Copyright 2001 University of Cambridge
+*)
header{*Decomposition of Analz into two parts*}
--- a/src/HOL/Auth/Guard/Extensions.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/HOL/Auth/Guard/Extensions.thy Sat Feb 19 08:39:05 2011 +0100
@@ -1,13 +1,7 @@
-(******************************************************************************
-date: november 2001
-author: Frederic Blanqui
-email: blanqui@lri.fr
-webpage: http://www.lri.fr/~blanqui/
-
-University of Cambridge, Computer Laboratory
-William Gates Building, JJ Thomson Avenue
-Cambridge CB3 0FD, United Kingdom
-******************************************************************************)
+(* Title: HOL/Auth/Guard/Extensions.thy
+ Author: Frederic Blanqui, University of Cambridge Computer Laboratory
+ Copyright 2001 University of Cambridge
+*)
header {*Extensions to Standard Theories*}
--- a/src/HOL/Auth/Guard/Guard.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/HOL/Auth/Guard/Guard.thy Sat Feb 19 08:39:05 2011 +0100
@@ -1,13 +1,7 @@
-(******************************************************************************
-date: january 2002
-author: Frederic Blanqui
-email: blanqui@lri.fr
-webpage: http://www.lri.fr/~blanqui/
-
-University of Cambridge, Computer Laboratory
-William Gates Building, JJ Thomson Avenue
-Cambridge CB3 0FD, United Kingdom
-******************************************************************************)
+(* Title: HOL/Auth/Guard/Guard.thy
+ Author: Frederic Blanqui, University of Cambridge Computer Laboratory
+ Copyright 2002 University of Cambridge
+*)
header{*Protocol-Independent Confidentiality Theorem on Nonces*}
--- a/src/HOL/Auth/Guard/GuardK.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/HOL/Auth/Guard/GuardK.thy Sat Feb 19 08:39:05 2011 +0100
@@ -1,18 +1,12 @@
-(******************************************************************************
-very similar to Guard except:
+(* Title: HOL/Auth/Guard/GuardK.thy
+ Author: Frederic Blanqui, University of Cambridge Computer Laboratory
+ Copyright 2002 University of Cambridge
+
+Very similar to Guard except:
- Guard is replaced by GuardK, guard by guardK, Nonce by Key
- some scripts are slightly modified (+ keyset_in, kparts_parts)
- the hypothesis Key n ~:G (keyset G) is added
-
-date: march 2002
-author: Frederic Blanqui
-email: blanqui@lri.fr
-webpage: http://www.lri.fr/~blanqui/
-
-University of Cambridge, Computer Laboratory
-William Gates Building, JJ Thomson Avenue
-Cambridge CB3 0FD, United Kingdom
-******************************************************************************)
+*)
header{*protocol-independent confidentiality theorem on keys*}
--- a/src/HOL/Auth/Guard/Guard_NS_Public.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/HOL/Auth/Guard/Guard_NS_Public.thy Sat Feb 19 08:39:05 2011 +0100
@@ -1,15 +1,9 @@
-(******************************************************************************
-incorporating Lowe's fix (inclusion of B's identity in round 2)
+(* Title: HOL/Auth/Guard/Guard_NS_Public.thy
+ Author: Frederic Blanqui, University of Cambridge Computer Laboratory
+ Copyright 2002 University of Cambridge
-date: march 2002
-author: Frederic Blanqui
-email: blanqui@lri.fr
-webpage: http://www.lri.fr/~blanqui/
-
-University of Cambridge, Computer Laboratory
-William Gates Building, JJ Thomson Avenue
-Cambridge CB3 0FD, United Kingdom
-******************************************************************************)
+Incorporating Lowe's fix (inclusion of B's identity in round 2).
+*)
header{*Needham-Schroeder-Lowe Public-Key Protocol*}
--- a/src/HOL/Auth/Guard/Guard_OtwayRees.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/HOL/Auth/Guard/Guard_OtwayRees.thy Sat Feb 19 08:39:05 2011 +0100
@@ -1,13 +1,7 @@
-(******************************************************************************
-date: march 2002
-author: Frederic Blanqui
-email: blanqui@lri.fr
-webpage: http://www.lri.fr/~blanqui/
-
-University of Cambridge, Computer Laboratory
-William Gates Building, JJ Thomson Avenue
-Cambridge CB3 0FD, United Kingdom
-******************************************************************************)
+(* Title: HOL/Auth/Guard/Guard_OtwayRees.thy
+ Author: Frederic Blanqui, University of Cambridge Computer Laboratory
+ Copyright 2002 University of Cambridge
+*)
header{*Otway-Rees Protocol*}
--- a/src/HOL/Auth/Guard/Guard_Public.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/HOL/Auth/Guard/Guard_Public.thy Sat Feb 19 08:39:05 2011 +0100
@@ -1,15 +1,9 @@
-(******************************************************************************
-lemmas on guarded messages for public protocols
+(* Title: HOL/Auth/Guard/Guard_Public.thy
+ Author: Frederic Blanqui, University of Cambridge Computer Laboratory
+ Copyright 2002 University of Cambridge
-date: march 2002
-author: Frederic Blanqui
-email: blanqui@lri.fr
-webpage: http://www.lri.fr/~blanqui/
-
-University of Cambridge, Computer Laboratory
-William Gates Building, JJ Thomson Avenue
-Cambridge CB3 0FD, United Kingdom
-******************************************************************************)
+Lemmas on guarded messages for public protocols.
+*)
theory Guard_Public imports Guard Public Extensions begin
--- a/src/HOL/Auth/Guard/Guard_Shared.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/HOL/Auth/Guard/Guard_Shared.thy Sat Feb 19 08:39:05 2011 +0100
@@ -1,13 +1,7 @@
-(******************************************************************************
-date: march 2002
-author: Frederic Blanqui
-email: blanqui@lri.fr
-webpage: http://www.lri.fr/~blanqui/
-
-University of Cambridge, Computer Laboratory
-William Gates Building, JJ Thomson Avenue
-Cambridge CB3 0FD, United Kingdom
-******************************************************************************)
+(* Title: HOL/Auth/Guard/Guard_Shared.thy
+ Author: Frederic Blanqui, University of Cambridge Computer Laboratory
+ Copyright 2002 University of Cambridge
+*)
header{*lemmas on guarded messages for protocols with symmetric keys*}
--- a/src/HOL/Auth/Guard/Guard_Yahalom.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/HOL/Auth/Guard/Guard_Yahalom.thy Sat Feb 19 08:39:05 2011 +0100
@@ -1,13 +1,7 @@
-(******************************************************************************
-date: march 2002
-author: Frederic Blanqui
-email: blanqui@lri.fr
-webpage: http://www.lri.fr/~blanqui/
-
-University of Cambridge, Computer Laboratory
-William Gates Building, JJ Thomson Avenue
-Cambridge CB3 0FD, United Kingdom
-******************************************************************************)
+(* Title: HOL/Auth/Guard/Guard_Yahalom.thy
+ Author: Frederic Blanqui, University of Cambridge Computer Laboratory
+ Copyright 2002 University of Cambridge
+*)
header{*Yahalom Protocol*}
--- a/src/HOL/Auth/Guard/List_Msg.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/HOL/Auth/Guard/List_Msg.thy Sat Feb 19 08:39:05 2011 +0100
@@ -1,13 +1,7 @@
-(******************************************************************************
-date: november 2001
-author: Frederic Blanqui
-email: blanqui@lri.fr
-webpage: http://www.lri.fr/~blanqui/
-
-University of Cambridge, Computer Laboratory
-William Gates Building, JJ Thomson Avenue
-Cambridge CB3 0FD, United Kingdom
-******************************************************************************)
+(* Title: HOL/Auth/Guard/List_Msg.thy
+ Author: Frederic Blanqui, University of Cambridge Computer Laboratory
+ Copyright 2001 University of Cambridge
+*)
header{*Lists of Messages and Lists of Agents*}
--- a/src/HOL/Auth/Guard/P1.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/HOL/Auth/Guard/P1.thy Sat Feb 19 08:39:05 2011 +0100
@@ -1,17 +1,11 @@
-(******************************************************************************
-from G. Karjoth, N. Asokan and C. Gulcu
-"Protecting the computation results of free-roaming agents"
-Mobiles Agents 1998, LNCS 1477
+(* Title: HOL/Auth/Guard/P1.thy
+ Author: Frederic Blanqui, University of Cambridge Computer Laboratory
+ Copyright 2002 University of Cambridge
-date: february 2002
-author: Frederic Blanqui
-email: blanqui@lri.fr
-webpage: http://www.lri.fr/~blanqui/
-
-University of Cambridge, Computer Laboratory
-William Gates Building, JJ Thomson Avenue
-Cambridge CB3 0FD, United Kingdom
-******************************************************************************)
+From G. Karjoth, N. Asokan and C. Gulcu
+"Protecting the computation results of free-roaming agents"
+Mobiles Agents 1998, LNCS 1477.
+*)
header{*Protocol P1*}
--- a/src/HOL/Auth/Guard/P2.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/HOL/Auth/Guard/P2.thy Sat Feb 19 08:39:05 2011 +0100
@@ -1,17 +1,11 @@
-(******************************************************************************
-from G. Karjoth, N. Asokan and C. Gulcu
-"Protecting the computation results of free-roaming agents"
-Mobiles Agents 1998, LNCS 1477
+(* Title: HOL/Auth/Guard/P2.thy
+ Author: Frederic Blanqui, University of Cambridge Computer Laboratory
+ Copyright 2002 University of Cambridge
-date: march 2002
-author: Frederic Blanqui
-email: blanqui@lri.fr
-webpage: http://www.lri.fr/~blanqui/
-
-University of Cambridge, Computer Laboratory
-William Gates Building, JJ Thomson Avenue
-Cambridge CB3 0FD, United Kingdom
-******************************************************************************)
+From G. Karjoth, N. Asokan and C. Gulcu
+"Protecting the computation results of free-roaming agents"
+Mobiles Agents 1998, LNCS 1477.
+*)
header{*Protocol P2*}
--- a/src/HOL/Auth/Guard/Proto.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/HOL/Auth/Guard/Proto.thy Sat Feb 19 08:39:05 2011 +0100
@@ -1,13 +1,7 @@
-(******************************************************************************
-date: april 2002
-author: Frederic Blanqui
-email: blanqui@lri.fr
-webpage: http://www.lri.fr/~blanqui/
-
-University of Cambridge, Computer Laboratory
-William Gates Building, JJ Thomson Avenue
-Cambridge CB3 0FD, United Kingdom
-******************************************************************************)
+(* Title: HOL/Auth/Guard/Proto.thy
+ Author: Frederic Blanqui, University of Cambridge Computer Laboratory
+ Copyright 2002 University of Cambridge
+*)
header{*Other Protocol-Independent Results*}
@@ -15,13 +9,13 @@
subsection{*protocols*}
-types rule = "event set * event"
+type_synonym rule = "event set * event"
abbreviation
msg' :: "rule => msg" where
"msg' R == msg (snd R)"
-types proto = "rule set"
+type_synonym proto = "rule set"
definition wdef :: "proto => bool" where
"wdef p == ALL R k. R:p --> Number k:parts {msg' R}
@@ -155,9 +149,9 @@
subsection{*types*}
-types keyfun = "rule => subs => nat => event list => key set"
+type_synonym keyfun = "rule => subs => nat => event list => key set"
-types secfun = "rule => nat => subs => key set => msg"
+type_synonym secfun = "rule => nat => subs => key set => msg"
subsection{*introduction of a fresh guarded nonce*}
--- a/src/HOL/Auth/KerberosIV.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/HOL/Auth/KerberosIV.thy Sat Feb 19 08:39:05 2011 +0100
@@ -16,7 +16,7 @@
Tgs :: agent where "Tgs == Friend 0"
-axioms
+axiomatization where
Tgs_not_bad [iff]: "Tgs \<notin> bad"
--{*Tgs is secure --- we already know that Kas is secure*}
--- a/src/HOL/Auth/KerberosIV_Gets.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/HOL/Auth/KerberosIV_Gets.thy Sat Feb 19 08:39:05 2011 +0100
@@ -16,7 +16,7 @@
Tgs :: agent where "Tgs == Friend 0"
-axioms
+axiomatization where
Tgs_not_bad [iff]: "Tgs \<notin> bad"
--{*Tgs is secure --- we already know that Kas is secure*}
--- a/src/HOL/Auth/KerberosV.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/HOL/Auth/KerberosV.thy Sat Feb 19 08:39:05 2011 +0100
@@ -17,7 +17,7 @@
"Tgs == Friend 0"
-axioms
+axiomatization where
Tgs_not_bad [iff]: "Tgs \<notin> bad"
--{*Tgs is secure --- we already know that Kas is secure*}
--- a/src/HOL/Auth/Message.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/HOL/Auth/Message.thy Sat Feb 19 08:39:05 2011 +0100
@@ -16,7 +16,7 @@
lemma [simp] : "A \<union> (B \<union> A) = B \<union> A"
by blast
-types
+type_synonym
key = nat
consts
--- a/src/HOL/Auth/Public.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/HOL/Auth/Public.thy Sat Feb 19 08:39:05 2011 +0100
@@ -68,7 +68,7 @@
done
-axioms
+axiomatization where
(*No private key equals any public key (essential to ensure that private
keys are private!) *)
privateKey_neq_publicKey [iff]: "privateKey b A \<noteq> publicKey c A'"
@@ -141,7 +141,7 @@
apply (simp add: inj_on_def split: agent.split)
done
-axioms
+axiomatization where
sym_shrK [iff]: "shrK X \<in> symKeys" --{*All shared keys are symmetric*}
text{*Injectiveness: Agents' long-term keys are distinct.*}
--- a/src/HOL/Auth/Smartcard/ShoupRubin.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/HOL/Auth/Smartcard/ShoupRubin.thy Sat Feb 19 08:39:05 2011 +0100
@@ -5,24 +5,19 @@
theory ShoupRubin imports Smartcard begin
-consts
-
- sesK :: "nat*key => key"
-
-axioms
-
+axiomatization sesK :: "nat*key => key"
+where
(*sesK is injective on each component*)
- inj_sesK [iff]: "(sesK(m,k) = sesK(m',k')) = (m = m' \<and> k = k')"
-
+ inj_sesK [iff]: "(sesK(m,k) = sesK(m',k')) = (m = m' \<and> k = k')" and
(*all long-term keys differ from sesK*)
- shrK_disj_sesK [iff]: "shrK A \<noteq> sesK(m,pk)"
- crdK_disj_sesK [iff]: "crdK C \<noteq> sesK(m,pk)"
- pin_disj_sesK [iff]: "pin P \<noteq> sesK(m,pk)"
- pairK_disj_sesK[iff]:"pairK(A,B) \<noteq> sesK(m,pk)"
+ shrK_disj_sesK [iff]: "shrK A \<noteq> sesK(m,pk)" and
+ crdK_disj_sesK [iff]: "crdK C \<noteq> sesK(m,pk)" and
+ pin_disj_sesK [iff]: "pin P \<noteq> sesK(m,pk)" and
+ pairK_disj_sesK[iff]:"pairK(A,B) \<noteq> sesK(m,pk)" and
(*needed for base case in analz_image_freshK*)
Atomic_distrib [iff]: "Atomic`(KEY`K \<union> NONCE`N) =
- Atomic`(KEY`K) \<union> Atomic`(NONCE`N)"
+ Atomic`(KEY`K) \<union> Atomic`(NONCE`N)" and
(*this protocol makes the assumption of secure means
between each agent and his smartcard*)
--- a/src/HOL/Auth/Smartcard/ShoupRubinBella.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/HOL/Auth/Smartcard/ShoupRubinBella.thy Sat Feb 19 08:39:05 2011 +0100
@@ -11,24 +11,20 @@
Availability. Only the updated version makes the goals of confidentiality,
authentication and key distribution available to both peers.*}
-consts
-
- sesK :: "nat*key => key"
-
-axioms
-
+axiomatization sesK :: "nat*key => key"
+where
(*sesK is injective on each component*)
- inj_sesK [iff]: "(sesK(m,k) = sesK(m',k')) = (m = m' \<and> k = k')"
+ inj_sesK [iff]: "(sesK(m,k) = sesK(m',k')) = (m = m' \<and> k = k')" and
(*all long-term keys differ from sesK*)
- shrK_disj_sesK [iff]: "shrK A \<noteq> sesK(m,pk)"
- crdK_disj_sesK [iff]: "crdK C \<noteq> sesK(m,pk)"
- pin_disj_sesK [iff]: "pin P \<noteq> sesK(m,pk)"
- pairK_disj_sesK[iff]: "pairK(A,B) \<noteq> sesK(m,pk)"
+ shrK_disj_sesK [iff]: "shrK A \<noteq> sesK(m,pk)" and
+ crdK_disj_sesK [iff]: "crdK C \<noteq> sesK(m,pk)" and
+ pin_disj_sesK [iff]: "pin P \<noteq> sesK(m,pk)" and
+ pairK_disj_sesK[iff]: "pairK(A,B) \<noteq> sesK(m,pk)" and
(*needed for base case in analz_image_freshK*)
Atomic_distrib [iff]: "Atomic`(KEY`K \<union> NONCE`N) =
- Atomic`(KEY`K) \<union> Atomic`(NONCE`N)"
+ Atomic`(KEY`K) \<union> Atomic`(NONCE`N)" and
(*this protocol makes the assumption of secure means
between each agent and his smartcard*)
--- a/src/HOL/Auth/Smartcard/Smartcard.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/HOL/Auth/Smartcard/Smartcard.thy Sat Feb 19 08:39:05 2011 +0100
@@ -16,31 +16,30 @@
smartcard, which independently may be stolen or cloned.
*}
-consts
- shrK :: "agent => key" (*long-term keys saved in smart cards*)
- crdK :: "card => key" (*smart cards' symmetric keys*)
- pin :: "agent => key" (*pin to activate the smart cards*)
+axiomatization
+ shrK :: "agent => key" and (*long-term keys saved in smart cards*)
+ crdK :: "card => key" and (*smart cards' symmetric keys*)
+ pin :: "agent => key" and (*pin to activate the smart cards*)
(*Mostly for Shoup-Rubin*)
- Pairkey :: "agent * agent => nat"
+ Pairkey :: "agent * agent => nat" and
pairK :: "agent * agent => key"
-
-axioms
- inj_shrK: "inj shrK" --{*No two smartcards store the same key*}
- inj_crdK: "inj crdK" --{*Nor do two cards*}
- inj_pin : "inj pin" --{*Nor do two agents have the same pin*}
+where
+ inj_shrK: "inj shrK" and --{*No two smartcards store the same key*}
+ inj_crdK: "inj crdK" and --{*Nor do two cards*}
+ inj_pin : "inj pin" and --{*Nor do two agents have the same pin*}
(*pairK is injective on each component, if we assume encryption to be a PRF
or at least collision free *)
- inj_pairK [iff]: "(pairK(A,B) = pairK(A',B')) = (A = A' & B = B')"
- comm_Pairkey [iff]: "Pairkey(A,B) = Pairkey(B,A)"
+ inj_pairK [iff]: "(pairK(A,B) = pairK(A',B')) = (A = A' & B = B')" and
+ comm_Pairkey [iff]: "Pairkey(A,B) = Pairkey(B,A)" and
(*long-term keys differ from each other*)
- pairK_disj_crdK [iff]: "pairK(A,B) \<noteq> crdK C"
- pairK_disj_shrK [iff]: "pairK(A,B) \<noteq> shrK P"
- pairK_disj_pin [iff]: "pairK(A,B) \<noteq> pin P"
- shrK_disj_crdK [iff]: "shrK P \<noteq> crdK C"
- shrK_disj_pin [iff]: "shrK P \<noteq> pin Q"
+ pairK_disj_crdK [iff]: "pairK(A,B) \<noteq> crdK C" and
+ pairK_disj_shrK [iff]: "pairK(A,B) \<noteq> shrK P" and
+ pairK_disj_pin [iff]: "pairK(A,B) \<noteq> pin P" and
+ shrK_disj_crdK [iff]: "shrK P \<noteq> crdK C" and
+ shrK_disj_pin [iff]: "shrK P \<noteq> pin Q" and
crdK_disj_pin [iff]: "crdK C \<noteq> pin P"
definition legalUse :: "card => bool" ("legalUse (_)") where
@@ -78,8 +77,8 @@
end
text{*Still relying on axioms*}
-axioms
- Key_supply_ax: "finite KK \<Longrightarrow> \<exists> K. K \<notin> KK & Key K \<notin> used evs"
+axiomatization where
+ Key_supply_ax: "finite KK \<Longrightarrow> \<exists> K. K \<notin> KK & Key K \<notin> used evs" and
(*Needed because of Spy's knowledge of Pairkeys*)
Nonce_supply_ax: "finite NN \<Longrightarrow> \<exists> N. N \<notin> NN & Nonce N \<notin> used evs"
@@ -129,7 +128,7 @@
(*Specialized to shared-key model: no @{term invKey}*)
lemma keysFor_parts_insert:
"\<lbrakk> K \<in> keysFor (parts (insert X G)); X \<in> synth (analz H) \<rbrakk>
- \<Longrightarrow> K \<in> keysFor (parts (G \<union> H)) | Key K \<in> parts H";
+ \<Longrightarrow> K \<in> keysFor (parts (G \<union> H)) | Key K \<in> parts H"
by (force dest: EventSC.keysFor_parts_insert)
lemma Crypt_imp_keysFor: "Crypt K X \<in> H \<Longrightarrow> K \<in> keysFor H"
--- a/src/HOL/Auth/TLS.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/HOL/Auth/TLS.thy Sat Feb 19 08:39:05 2011 +0100
@@ -86,9 +86,9 @@
apply (simp add: inj_on_def prod_encode_eq split: role.split)
done
-axioms
+axiomatization where
--{*sessionK makes symmetric keys*}
- isSym_sessionK: "sessionK nonces \<in> symKeys"
+ isSym_sessionK: "sessionK nonces \<in> symKeys" and
--{*sessionK never clashes with a long-term symmetric key
(they don't exist in TLS anyway)*}
--- a/src/HOL/Bali/AxSem.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/HOL/Bali/AxSem.thy Sat Feb 19 08:39:05 2011 +0100
@@ -36,7 +36,7 @@
\end{itemize}
*}
-types res = vals --{* result entry *}
+type_synonym res = vals --{* result entry *}
abbreviation (input)
Val where "Val x == In1 x"
@@ -58,7 +58,7 @@
"\<lambda>Vals:v. b" == "(\<lambda>v. b) \<circ> CONST the_In3"
--{* relation on result values, state and auxiliary variables *}
-types 'a assn = "res \<Rightarrow> state \<Rightarrow> 'a \<Rightarrow> bool"
+type_synonym 'a assn = "res \<Rightarrow> state \<Rightarrow> 'a \<Rightarrow> bool"
translations
(type) "'a assn" <= (type) "vals \<Rightarrow> state \<Rightarrow> 'a \<Rightarrow> bool"
@@ -381,7 +381,7 @@
datatype 'a triple = triple "('a assn)" "term" "('a assn)" (** should be
something like triple = \<forall>'a. triple ('a assn) term ('a assn) **)
("{(1_)}/ _>/ {(1_)}" [3,65,3]75)
-types 'a triples = "'a triple set"
+type_synonym 'a triples = "'a triple set"
abbreviation
var_triple :: "['a assn, var ,'a assn] \<Rightarrow> 'a triple"
--- a/src/HOL/Bali/Conform.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/HOL/Bali/Conform.thy Sat Feb 19 08:39:05 2011 +0100
@@ -16,7 +16,7 @@
\end{itemize}
*}
-types env' = "prog \<times> (lname, ty) table" (* same as env of WellType.thy *)
+type_synonym env' = "prog \<times> (lname, ty) table" (* same as env of WellType.thy *)
section "extension of global store"
--- a/src/HOL/Bali/Decl.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/HOL/Bali/Decl.thy Sat Feb 19 08:39:05 2011 +0100
@@ -136,7 +136,7 @@
subsubsection {* Static Modifier *}
-types stat_modi = bool (* modifier: static *)
+type_synonym stat_modi = bool (* modifier: static *)
subsection {* Declaration (base "class" for member,interface and class
declarations *}
@@ -164,8 +164,7 @@
(type) "field" <= (type) "\<lparr>access::acc_modi, static::bool, type::ty\<rparr>"
(type) "field" <= (type) "\<lparr>access::acc_modi, static::bool, type::ty,\<dots>::'a\<rparr>"
-types
- fdecl (* field declaration, cf. 8.3 *)
+type_synonym fdecl (* field declaration, cf. 8.3 *)
= "vname \<times> field"
@@ -185,7 +184,7 @@
record methd = mhead + (* method in a class *)
mbody::mbody
-types mdecl = "sig \<times> methd" (* method declaration in a class *)
+type_synonym mdecl = "sig \<times> methd" (* method declaration in a class *)
translations
@@ -300,7 +299,7 @@
record iface = ibody + --{* interface *}
isuperIfs:: "qtname list" --{* superinterface list *}
-types
+type_synonym
idecl --{* interface declaration, cf. 9.1 *}
= "qtname \<times> iface"
@@ -332,7 +331,7 @@
record "class" = cbody + --{* class *}
super :: "qtname" --{* superclass *}
superIfs:: "qtname list" --{* implemented interfaces *}
-types
+type_synonym
cdecl --{* class declaration, cf. 8.1 *}
= "qtname \<times> class"
--- a/src/HOL/Bali/DeclConcepts.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/HOL/Bali/DeclConcepts.thy Sat Feb 19 08:39:05 2011 +0100
@@ -1401,7 +1401,7 @@
section "fields and methods"
-types
+type_synonym
fspec = "vname \<times> qtname"
translations
--- a/src/HOL/Bali/DefiniteAssignment.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/HOL/Bali/DefiniteAssignment.thy Sat Feb 19 08:39:05 2011 +0100
@@ -498,7 +498,7 @@
section "The rules of definite assignment"
-types breakass = "(label, lname) tables"
+type_synonym breakass = "(label, lname) tables"
--{* Mapping from a break label, to the set of variables that will be assigned
if the evaluation terminates with this break *}
--- a/src/HOL/Bali/Eval.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/HOL/Bali/Eval.thy Sat Feb 19 08:39:05 2011 +0100
@@ -96,8 +96,8 @@
*}
-types vvar = "val \<times> (val \<Rightarrow> state \<Rightarrow> state)"
- vals = "(val, vvar, val list) sum3"
+type_synonym vvar = "val \<times> (val \<Rightarrow> state \<Rightarrow> state)"
+type_synonym vals = "(val, vvar, val list) sum3"
translations
(type) "vvar" <= (type) "val \<times> (val \<Rightarrow> state \<Rightarrow> state)"
(type) "vals" <= (type) "(val, vvar, val list) sum3"
--- a/src/HOL/Bali/State.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/HOL/Bali/State.thy Sat Feb 19 08:39:05 2011 +0100
@@ -27,7 +27,7 @@
since its type is given already by the reference to
it (see below) *}
-types vn = "fspec + int" --{* variable name *}
+type_synonym vn = "fspec + int" --{* variable name *}
record obj =
tag :: "obj_tag" --{* generalized object *}
"values" :: "(vn, val) table"
@@ -130,7 +130,7 @@
section "object references"
-types oref = "loc + qtname" --{* generalized object reference *}
+type_synonym oref = "loc + qtname" --{* generalized object reference *}
syntax
Heap :: "loc \<Rightarrow> oref"
Stat :: "qtname \<Rightarrow> oref"
@@ -213,11 +213,11 @@
section "stores"
-types globs --{* global variables: heap and static variables *}
+type_synonym globs --{* global variables: heap and static variables *}
= "(oref , obj) table"
- heap
+type_synonym heap
= "(loc , obj) table"
-(* locals
+(* type_synonym locals
= "(lname, val) table" *) (* defined in Value.thy local variables *)
translations
@@ -579,7 +579,7 @@
section "full program state"
-types
+type_synonym
state = "abopt \<times> st" --{* state including abruption information *}
translations
--- a/src/HOL/Bali/Table.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/HOL/Bali/Table.thy Sat Feb 19 08:39:05 2011 +0100
@@ -29,9 +29,9 @@
\end{itemize}
*}
-types ('a, 'b) table --{* table with key type 'a and contents type 'b *}
+type_synonym ('a, 'b) table --{* table with key type 'a and contents type 'b *}
= "'a \<rightharpoonup> 'b"
- ('a, 'b) tables --{* non-unique table with key 'a and contents 'b *}
+type_synonym ('a, 'b) tables --{* non-unique table with key 'a and contents 'b *}
= "'a \<Rightarrow> 'b set"
--- a/src/HOL/Bali/Term.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/HOL/Bali/Term.thy Sat Feb 19 08:39:05 2011 +0100
@@ -57,7 +57,7 @@
-types locals = "(lname, val) table" --{* local variables *}
+type_synonym locals = "(lname, val) table" --{* local variables *}
datatype jump
@@ -78,7 +78,7 @@
| Jump jump --{* break, continue, return *}
| Error error -- {* runtime errors, we wan't to detect and proof absent
in welltyped programms *}
-types
+type_synonym
abopt = "abrupt option"
text {* Local variable store and exception.
@@ -235,7 +235,7 @@
intermediate steps of class-initialisation.
*}
-types "term" = "(expr+stmt,var,expr list) sum3"
+type_synonym "term" = "(expr+stmt,var,expr list) sum3"
translations
(type) "sig" <= (type) "mname \<times> ty list"
(type) "term" <= (type) "(expr+stmt,var,expr list) sum3"
--- a/src/HOL/Bali/Value.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/HOL/Bali/Value.thy Sat Feb 19 08:39:05 2011 +0100
@@ -26,7 +26,7 @@
primrec the_Addr :: "val \<Rightarrow> loc"
where "the_Addr (Addr a) = a"
-types dyn_ty = "loc \<Rightarrow> ty option"
+type_synonym dyn_ty = "loc \<Rightarrow> ty option"
primrec typeof :: "dyn_ty \<Rightarrow> val \<Rightarrow> ty option"
where
--- a/src/HOL/Bali/WellType.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/HOL/Bali/WellType.thy Sat Feb 19 08:39:05 2011 +0100
@@ -28,7 +28,7 @@
\end{itemize}
*}
-types lenv
+type_synonym lenv
= "(lname, ty) table" --{* local variables, including This and Result*}
record env =
@@ -49,7 +49,7 @@
section "Static overloading: maximally specific methods "
-types
+type_synonym
emhead = "ref_ty \<times> mhead"
--{* Some mnemotic selectors for emhead *}
@@ -244,7 +244,7 @@
section "Typing for terms"
-types tys = "ty + ty list"
+type_synonym tys = "ty + ty list"
translations
(type) "tys" <= (type) "ty + ty list"
--- a/src/HOL/Tools/ATP/atp_problem.ML Thu Feb 17 09:31:29 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_problem.ML Sat Feb 19 08:39:05 2011 +0100
@@ -16,8 +16,9 @@
AAtom of 'b
type 'a uniform_formula = ('a, 'a fo_term) formula
- datatype kind = Axiom | Hypothesis | Conjecture
- datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula
+ datatype kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
+ datatype 'a problem_line =
+ Fof of string * kind * ('a, 'a fo_term) formula * string fo_term option
type 'a problem = (string * 'a problem_line list) list
val timestamp : unit -> string
@@ -44,19 +45,25 @@
AAtom of 'b
type 'a uniform_formula = ('a, 'a fo_term) formula
-datatype kind = Axiom | Hypothesis | Conjecture
-datatype 'a problem_line = Fof of string * kind * ('a, 'a fo_term) formula
+datatype kind = Axiom | Definition | Lemma | Hypothesis | Conjecture
+datatype 'a problem_line =
+ Fof of string * kind * ('a, 'a fo_term) formula * string fo_term option
type 'a problem = (string * 'a problem_line list) list
val timestamp = Date.fmt "%Y-%m-%d %H:%M:%S" o Date.fromTimeLocal o Time.now
fun string_for_kind Axiom = "axiom"
+ | string_for_kind Definition = "definition"
+ | string_for_kind Lemma = "lemma"
| string_for_kind Hypothesis = "hypothesis"
| string_for_kind Conjecture = "conjecture"
fun string_for_term (ATerm (s, [])) = s
| string_for_term (ATerm ("equal", ts)) =
space_implode " = " (map string_for_term ts)
+ | string_for_term (ATerm ("[]", ts)) =
+ (* used for lists in the optional "source" field of a derivation *)
+ "[" ^ commas (map string_for_term ts) ^ "]"
| string_for_term (ATerm (s, ts)) =
s ^ "(" ^ commas (map string_for_term ts) ^ ")"
fun string_for_quantifier AForall = "!"
@@ -81,7 +88,7 @@
| string_for_formula (AAtom tm) = string_for_term tm
fun string_for_problem_line use_conjecture_for_hypotheses
- (Fof (ident, kind, phi)) =
+ (Fof (ident, kind, phi, source)) =
let
val (kind, phi) =
if kind = Hypothesis andalso use_conjecture_for_hypotheses then
@@ -90,7 +97,10 @@
(kind, phi)
in
"fof(" ^ ident ^ ", " ^ string_for_kind kind ^ ",\n (" ^
- string_for_formula phi ^ ")).\n"
+ string_for_formula phi ^ ")" ^
+ (case source of
+ SOME tm => ", " ^ string_for_term tm
+ | NONE => "") ^ ").\n"
end
fun tptp_strings_for_atp_problem use_conjecture_for_hypotheses problem =
"% This file was generated by Isabelle (most likely Sledgehammer)\n\
@@ -160,8 +170,8 @@
| nice_formula (AConn (c, phis)) =
pool_map nice_formula phis #>> curry AConn c
| nice_formula (AAtom tm) = nice_term tm #>> AAtom
-fun nice_problem_line (Fof (ident, kind, phi)) =
- nice_formula phi #>> (fn phi => Fof (ident, kind, phi))
+fun nice_problem_line (Fof (ident, kind, phi, source)) =
+ nice_formula phi #>> (fn phi => Fof (ident, kind, phi, source))
fun nice_problem problem =
pool_map (fn (heading, lines) =>
pool_map nice_problem_line lines #>> pair heading) problem
--- a/src/HOL/Tools/ATP/atp_systems.ML Thu Feb 17 09:31:29 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_systems.ML Sat Feb 19 08:39:05 2011 +0100
@@ -26,10 +26,10 @@
val e_weight_method : e_weight_method Unsynchronized.ref
val e_default_fun_weight : real Unsynchronized.ref
val e_fun_weight_base : real Unsynchronized.ref
- val e_fun_weight_factor : real Unsynchronized.ref
+ val e_fun_weight_span : real Unsynchronized.ref
val e_default_sym_offs_weight : real Unsynchronized.ref
val e_sym_offs_weight_base : real Unsynchronized.ref
- val e_sym_offs_weight_factor : real Unsynchronized.ref
+ val e_sym_offs_weight_span : real Unsynchronized.ref
val eN : string
val spassN : string
@@ -109,12 +109,13 @@
datatype e_weight_method = E_Auto | E_Fun_Weight | E_Sym_Offset_Weight
val e_weight_method = Unsynchronized.ref E_Fun_Weight
-val e_default_fun_weight = Unsynchronized.ref 0.5
+(* FUDGE *)
+val e_default_fun_weight = Unsynchronized.ref 20.0
val e_fun_weight_base = Unsynchronized.ref 0.0
-val e_fun_weight_factor = Unsynchronized.ref 40.0
-val e_default_sym_offs_weight = Unsynchronized.ref 0.0
-val e_sym_offs_weight_base = Unsynchronized.ref ~30.0
-val e_sym_offs_weight_factor = Unsynchronized.ref ~30.0
+val e_fun_weight_span = Unsynchronized.ref 40.0
+val e_default_sym_offs_weight = Unsynchronized.ref 1.0
+val e_sym_offs_weight_base = Unsynchronized.ref ~20.0
+val e_sym_offs_weight_span = Unsynchronized.ref 60.0
fun e_weight_method_case fw sow =
case !e_weight_method of
@@ -124,7 +125,7 @@
fun scaled_e_weight w =
e_weight_method_case (!e_fun_weight_base) (!e_sym_offs_weight_base)
- + w * e_weight_method_case (!e_fun_weight_factor) (!e_sym_offs_weight_factor)
+ + w * e_weight_method_case (!e_fun_weight_span) (!e_sym_offs_weight_span)
|> Real.ceil |> signed_string_of_int
fun e_weight_arguments weights =
@@ -138,8 +139,8 @@
\--delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred \
\-H'(4*" ^ e_weight_method_case "FunWeight" "SymOffsetWeight" ^
"(SimulateSOS, " ^
- scaled_e_weight (e_weight_method_case (!e_default_fun_weight)
- (!e_default_sym_offs_weight)) ^
+ (e_weight_method_case (!e_default_fun_weight) (!e_default_sym_offs_weight)
+ |> Real.ceil |> signed_string_of_int) ^
",20,1.5,1.5,1" ^
(weights () |> map (fn (s, w) => "," ^ s ^ ":" ^ scaled_e_weight w)
|> implode) ^
--- a/src/HOL/Tools/Nitpick/nitpick.ML Thu Feb 17 09:31:29 2011 +0100
+++ b/src/HOL/Tools/Nitpick/nitpick.ML Sat Feb 19 08:39:05 2011 +0100
@@ -981,15 +981,15 @@
in (outcome_code, !state_ref) end
(* Give the inner timeout a chance. *)
-val timeout_bonus = seconds 0.25
+val timeout_bonus = seconds 1.0
fun pick_nits_in_term state (params as {debug, timeout, expect, ...}) auto i n
step subst assm_ts orig_t =
- let val warning_m = if auto then K () else warning in
+ let val print_m = if auto then K () else Output.urgent_message in
if getenv "KODKODI" = "" then
(* The "expect" argument is deliberately ignored if Kodkodi is missing so
that the "Nitpick_Examples" can be processed on any machine. *)
- (warning_m (Pretty.string_of (plazy install_kodkodi_message));
+ (print_m (Pretty.string_of (plazy install_kodkodi_message));
("no_kodkodi", state))
else
let
@@ -1001,12 +1001,14 @@
(pick_them_nits_in_term deadline state params auto i n step subst
assm_ts) orig_t
handle TOO_LARGE (_, details) =>
- (warning ("Limit reached: " ^ details ^ "."); unknown_outcome)
+ (print_m ("Limit reached: " ^ details ^ "."); unknown_outcome)
| TOO_SMALL (_, details) =>
- (warning ("Limit reached: " ^ details ^ "."); unknown_outcome)
+ (print_m ("Limit reached: " ^ details ^ "."); unknown_outcome)
| Kodkod.SYNTAX (_, details) =>
- (warning ("Ill-formed Kodkodi output: " ^ details ^ ".");
+ (print_m ("Malformed Kodkodi output: " ^ details ^ ".");
unknown_outcome)
+ | TimeLimit.TimeOut =>
+ (print_m "Nitpick ran out of time."; unknown_outcome)
in
if expect = "" orelse outcome_code = expect then outcome
else error ("Unexpected outcome: " ^ quote outcome_code ^ ".")
--- a/src/HOL/Tools/SMT/smt_setup_solvers.ML Thu Feb 17 09:31:29 2011 +0100
+++ b/src/HOL/Tools/SMT/smt_setup_solvers.ML Sat Feb 19 08:39:05 2011 +0100
@@ -62,7 +62,7 @@
avail = make_avail is_remote "CVC3",
command = make_command is_remote "CVC3",
options = cvc3_options,
- default_max_relevant = 250,
+ default_max_relevant = 200,
supports_filter = false,
outcome =
on_first_line (outcome_of "Unsatisfiable." "Satisfiable." "Unknown."),
@@ -86,7 +86,7 @@
options = (fn ctxt => [
"--rand-seed=" ^ string_of_int (Config.get ctxt SMT_Config.random_seed),
"--smtlib"]),
- default_max_relevant = 275,
+ default_max_relevant = 200,
supports_filter = false,
outcome = on_first_line (outcome_of "unsat" "sat" "unknown"),
cex_parser = NONE,
@@ -131,7 +131,7 @@
avail = make_avail is_remote "Z3",
command = z3_make_command is_remote "Z3",
options = z3_options,
- default_max_relevant = 225,
+ default_max_relevant = 250,
supports_filter = true,
outcome = z3_on_last_line,
cex_parser = SOME Z3_Model.parse_counterex,
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Thu Feb 17 09:31:29 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_atp_translate.ML Sat Feb 19 08:39:05 2011 +0100
@@ -294,7 +294,7 @@
in
[Fof (helper_prefix ^ ascii_of "ti_ti", Axiom,
AAtom (ATerm (`I "equal", [tag (tag (var "Y")), tag (var "Y")]))
- |> explicit_forall ? close_universally)]
+ |> explicit_forall ? close_universally, NONE)]
end
else
[])
@@ -440,14 +440,15 @@
(formula_for_combformula ctxt type_sys combformula)
fun problem_line_for_fact ctxt prefix type_sys (formula as {name, kind, ...}) =
- Fof (prefix ^ ascii_of name, kind, formula_for_fact ctxt type_sys formula)
+ Fof (prefix ^ ascii_of name, kind, formula_for_fact ctxt type_sys formula,
+ NONE)
fun problem_line_for_class_rel_clause (ClassRelClause {name, subclass,
superclass, ...}) =
let val ty_arg = ATerm (("T", "T"), []) in
Fof (class_rel_clause_prefix ^ ascii_of name, Axiom,
AConn (AImplies, [AAtom (ATerm (subclass, [ty_arg])),
- AAtom (ATerm (superclass, [ty_arg]))]))
+ AAtom (ATerm (superclass, [ty_arg]))]), NONE)
end
fun fo_literal_for_arity_literal (TConsLit (c, t, args)) =
@@ -461,12 +462,12 @@
mk_ahorn (map (formula_for_fo_literal o apfst not
o fo_literal_for_arity_literal) premLits)
(formula_for_fo_literal
- (fo_literal_for_arity_literal conclLit)))
+ (fo_literal_for_arity_literal conclLit)), NONE)
fun problem_line_for_conjecture ctxt type_sys
({name, kind, combformula, ...} : translated_formula) =
Fof (conjecture_prefix ^ name, kind,
- formula_for_combformula ctxt type_sys combformula)
+ formula_for_combformula ctxt type_sys combformula, NONE)
fun free_type_literals_for_conjecture type_sys
({ctypes_sorts, ...} : translated_formula) =
@@ -474,7 +475,8 @@
|> map fo_literal_for_type_literal
fun problem_line_for_free_type j lit =
- Fof (tfree_prefix ^ string_of_int j, Hypothesis, formula_for_fo_literal lit)
+ Fof (tfree_prefix ^ string_of_int j, Hypothesis, formula_for_fo_literal lit,
+ NONE)
fun problem_lines_for_free_types type_sys conjs =
let
val litss = map (free_type_literals_for_conjecture type_sys) conjs
@@ -502,7 +504,7 @@
| consider_formula (AConn (_, phis)) = fold consider_formula phis
| consider_formula (AAtom tm) = consider_term true tm
-fun consider_problem_line (Fof (_, _, phi)) = consider_formula phi
+fun consider_problem_line (Fof (_, _, phi, _)) = consider_formula phi
fun consider_problem problem = fold (fold consider_problem_line o snd) problem
(* needed for helper facts if the problem otherwise does not involve equality *)
@@ -593,8 +595,9 @@
in aux #> explicit_forall ? close_universally end
fun repair_problem_line thy explicit_forall type_sys const_tab
- (Fof (ident, kind, phi)) =
- Fof (ident, kind, repair_formula thy explicit_forall type_sys const_tab phi)
+ (Fof (ident, kind, phi, source)) =
+ Fof (ident, kind, repair_formula thy explicit_forall type_sys const_tab phi,
+ source)
fun repair_problem thy = map o apsnd o map ooo repair_problem_line thy
fun dest_Fof (Fof z) = z
@@ -647,14 +650,14 @@
(* FUDGE *)
val conj_weight = 0.0
-val hyp_weight = 0.05
-val fact_min_weight = 0.1
+val hyp_weight = 0.1
+val fact_min_weight = 0.2
val fact_max_weight = 1.0
fun add_term_weights weight (ATerm (s, tms)) =
(not (is_atp_variable s) andalso s <> "equal") ? Symtab.default (s, weight)
#> fold (add_term_weights weight) tms
-fun add_problem_line_weights weight (Fof (_, _, phi)) =
+fun add_problem_line_weights weight (Fof (_, _, phi, _)) =
fold_formula (add_term_weights weight) phi
fun add_conjectures_weights [] = I
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Thu Feb 17 09:31:29 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Sat Feb 19 08:39:05 2011 +0100
@@ -41,6 +41,9 @@
val all_facts :
Proof.context -> 'a Symtab.table -> bool -> relevance_fudge -> thm list
-> thm list -> (((unit -> string) * locality) * (bool * thm)) list
+ val const_names_in_fact :
+ theory -> (string * typ -> term list -> bool * term list) -> term
+ -> string list
val relevant_facts :
Proof.context -> bool -> real * real -> int
-> (string * typ -> term list -> bool * term list) -> relevance_fudge
@@ -467,6 +470,8 @@
[] => NONE
| consts => SOME ((fact, consts), NONE)
+val const_names_in_fact = map fst ooo pconsts_in_fact
+
type annotated_thm =
(((unit -> string) * locality) * thm) * (string * ptype) list
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Thu Feb 17 09:31:29 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_run.ML Sat Feb 19 08:39:05 2011 +0100
@@ -175,6 +175,7 @@
| n =>
let
val _ = Proof.assert_backward state
+ val print = if auto then K () else Output.urgent_message
val state =
state |> Proof.map_context (Config.put SMT_Config.verbose debug)
val ctxt = Proof.context_of state
@@ -186,7 +187,7 @@
val _ = case find_first (not o is_prover_supported ctxt) provers of
SOME name => error ("No such prover: " ^ name ^ ".")
| NONE => ()
- val _ = if auto then () else Output.urgent_message "Sledgehammering..."
+ val _ = print "Sledgehammering..."
val (smts, atps) = provers |> List.partition (is_smt_prover ctxt)
fun launch_provers state get_facts translate maybe_smt_filter provers =
let
@@ -234,7 +235,7 @@
"Including (up to) " ^ string_of_int (length facts) ^
" relevant fact" ^ plural_s (length facts) ^ ":\n" ^
(facts |> map (fst o fst) |> space_implode " ") ^ ".")
- |> Output.urgent_message
+ |> print
else
())
end
@@ -265,11 +266,13 @@
fun launch_atps_and_smt_solvers () =
[launch_atps, launch_smts]
|> smart_par_list_map (fn f => f (false, state) |> K ())
- handle ERROR msg => (Output.urgent_message ("Error: " ^ msg); error msg)
+ handle ERROR msg => (print ("Error: " ^ msg); error msg)
in
(false, state)
|> (if blocking then launch_atps #> not auto ? launch_smts
else (fn p => Future.fork (tap launch_atps_and_smt_solvers) |> K p))
+ handle TimeLimit.TimeOut =>
+ (print "Sledgehammer ran out of time."; (false, state))
end
end;
--- a/src/HOL/ZF/Games.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/HOL/ZF/Games.thy Sat Feb 19 08:39:05 2011 +0100
@@ -1,4 +1,4 @@
-(* Title: HOL/ZF/MainZF.thy/Games.thy
+(* Title: HOL/ZF/Games.thy
Author: Steven Obua
An application of HOLZF: Partizan Games. See "Partizan Games in
--- a/src/Pure/Concurrent/future.ML Thu Feb 17 09:31:29 2011 +0100
+++ b/src/Pure/Concurrent/future.ML Sat Feb 19 08:39:05 2011 +0100
@@ -203,7 +203,7 @@
Task_Queue.running task (fn () =>
setmp_worker_task task (fn () =>
fold (fn job => fn ok => job valid andalso ok) jobs true) ());
- val _ = Multithreading.tracing 1 (fn () =>
+ val _ = Multithreading.tracing 2 (fn () =>
let
val s = Task_Queue.str_of_task task;
fun micros time = string_of_int (Time.toNanoseconds time div 1000);
--- a/src/Pure/goal.ML Thu Feb 17 09:31:29 2011 +0100
+++ b/src/Pure/goal.ML Sat Feb 19 08:39:05 2011 +0100
@@ -115,7 +115,7 @@
let
val n = m + i;
val _ =
- Multithreading.tracing 1 (fn () =>
+ Multithreading.tracing 2 (fn () =>
("PROOFS " ^ Time.toString (Time.now ()) ^ ": " ^ string_of_int n));
in n end);
--- a/src/ZF/AC/AC17_AC1.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/ZF/AC/AC17_AC1.thy Sat Feb 19 08:39:05 2011 +0100
@@ -1,4 +1,4 @@
-(* Title: ZF/AC/AC1_AC17.thy
+(* Title: ZF/AC/AC17_AC1.thy
Author: Krzysztof Grabczewski
The equivalence of AC0, AC1 and AC17
--- a/src/ZF/ArithSimp.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/ZF/ArithSimp.thy Sat Feb 19 08:39:05 2011 +0100
@@ -1,4 +1,4 @@
-(* Title: ZF/ArithSimp.ML
+(* Title: ZF/ArithSimp.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 2000 University of Cambridge
*)
--- a/src/ZF/Bool.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/ZF/Bool.thy Sat Feb 19 08:39:05 2011 +0100
@@ -1,4 +1,4 @@
-(* Title: ZF/bool.thy
+(* Title: ZF/Bool.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge
*)
--- a/src/ZF/Coind/Language.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/ZF/Coind/Language.thy Sat Feb 19 08:39:05 2011 +0100
@@ -5,14 +5,14 @@
theory Language imports Main begin
-consts
- Const :: i (* Abstract type of constants *)
- c_app :: "[i,i] => i" (* Abstract constructor for fun application*)
-
text{*these really can't be definitions without losing the abstraction*}
-axioms
- constNEE: "c \<in> Const ==> c \<noteq> 0"
+
+axiomatization
+ Const :: i and (* Abstract type of constants *)
+ c_app :: "[i,i] => i" (* Abstract constructor for fun application*)
+where
+ constNEE: "c \<in> Const ==> c \<noteq> 0" and
c_appI: "[| c1 \<in> Const; c2 \<in> Const |] ==> c_app(c1,c2) \<in> Const"
--- a/src/ZF/Coind/Static.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/ZF/Coind/Static.thy Sat Feb 19 08:39:05 2011 +0100
@@ -9,11 +9,8 @@
parameter of the proof. A concrete version could be defined inductively.
***)
-consts
- isof :: "[i,i] => o"
-
-axioms
- isof_app: "[|isof(c1,t_fun(t1,t2)); isof(c2,t1)|] ==> isof(c_app(c1,c2),t2)"
+axiomatization isof :: "[i,i] => o"
+ where isof_app: "[|isof(c1,t_fun(t1,t2)); isof(c2,t1)|] ==> isof(c_app(c1,c2),t2)"
(*Its extension to environments*)
--- a/src/ZF/Datatype_ZF.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/ZF/Datatype_ZF.thy Sat Feb 19 08:39:05 2011 +0100
@@ -1,4 +1,4 @@
-(* Title: ZF/Datatype.thy
+(* Title: ZF/Datatype_ZF.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1997 University of Cambridge
*)
--- a/src/ZF/Int_ZF.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/ZF/Int_ZF.thy Sat Feb 19 08:39:05 2011 +0100
@@ -1,4 +1,4 @@
-(* Title: ZF/Int.thy
+(* Title: ZF/Int_ZF.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
*)
--- a/src/ZF/OrdQuant.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/ZF/OrdQuant.thy Sat Feb 19 08:39:05 2011 +0100
@@ -1,4 +1,4 @@
-(* Title: ZF/AC/OrdQuant.thy
+(* Title: ZF/OrdQuant.thy
Authors: Krzysztof Grabczewski and L C Paulson
*)
--- a/src/ZF/Sum.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/ZF/Sum.thy Sat Feb 19 08:39:05 2011 +0100
@@ -1,4 +1,4 @@
-(* Title: ZF/sum.thy
+(* Title: ZF/Sum.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1993 University of Cambridge
*)
--- a/src/ZF/UNITY/AllocBase.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/ZF/UNITY/AllocBase.thy Sat Feb 19 08:39:05 2011 +0100
@@ -7,17 +7,16 @@
theory AllocBase imports Follows MultisetSum Guar begin
-consts
- NbT :: i (* Number of tokens in system *)
- Nclients :: i (* Number of clients *)
-
abbreviation (input)
tokbag :: i (* tokbags could be multisets...or any ordered type?*)
where
"tokbag == nat"
-axioms
- NbT_pos: "NbT \<in> nat-{0}"
+axiomatization
+ NbT :: i and (* Number of tokens in system *)
+ Nclients :: i (* Number of clients *)
+where
+ NbT_pos: "NbT \<in> nat-{0}" and
Nclients_pos: "Nclients \<in> nat-{0}"
text{*This function merely sums the elements of a list*}
@@ -27,9 +26,7 @@
"tokens(Nil) = 0"
"tokens (Cons(x,xs)) = x #+ tokens(xs)"
-consts
- bag_of :: "i => i"
-
+consts bag_of :: "i => i"
primrec
"bag_of(Nil) = 0"
"bag_of(Cons(x,xs)) = {#x#} +# bag_of(xs)"
@@ -38,7 +35,7 @@
text{*Definitions needed in Client.thy. We define a recursive predicate
using 0 and 1 to code the truth values.*}
consts all_distinct0 :: "i=>i"
- primrec
+primrec
"all_distinct0(Nil) = 1"
"all_distinct0(Cons(a, l)) =
(if a \<in> set_of_list(l) then 0 else all_distinct0(l))"
--- a/src/ZF/UNITY/AllocImpl.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/ZF/UNITY/AllocImpl.thy Sat Feb 19 08:39:05 2011 +0100
@@ -16,9 +16,9 @@
available_tok :: i (*number of free tokens (T in paper)*) where
"available_tok == Var([succ(succ(2))])"
-axioms
+axiomatization where
alloc_type_assumes [simp]:
- "type_of(NbR) = nat & type_of(available_tok)=nat"
+ "type_of(NbR) = nat & type_of(available_tok)=nat" and
alloc_default_val_assumes [simp]:
"default_val(NbR) = 0 & default_val(available_tok)=0"
--- a/src/ZF/UNITY/ClientImpl.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/ZF/UNITY/ClientImpl.thy Sat Feb 19 08:39:05 2011 +0100
@@ -12,13 +12,13 @@
abbreviation "rel == Var([1])" (* input history: tokens released *)
abbreviation "tok == Var([2])" (* the number of available tokens *)
-axioms
+axiomatization where
type_assumes:
"type_of(ask) = list(tokbag) & type_of(giv) = list(tokbag) &
- type_of(rel) = list(tokbag) & type_of(tok) = nat"
+ type_of(rel) = list(tokbag) & type_of(tok) = nat" and
default_val_assumes:
- "default_val(ask) = Nil & default_val(giv) = Nil &
- default_val(rel) = Nil & default_val(tok) = 0"
+ "default_val(ask) = Nil & default_val(giv) = Nil &
+ default_val(rel) = Nil & default_val(tok) = 0"
(*Array indexing is translated to list indexing as A[n] == nth(n-1,A). *)
--- a/src/ZF/UNITY/Mutex.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/ZF/UNITY/Mutex.thy Sat Feb 19 08:39:05 2011 +0100
@@ -27,11 +27,11 @@
abbreviation "u == Var([0,1])"
abbreviation "v == Var([1,0])"
-axioms --{** Type declarations **}
- p_type: "type_of(p)=bool & default_val(p)=0"
- m_type: "type_of(m)=int & default_val(m)=#0"
- n_type: "type_of(n)=int & default_val(n)=#0"
- u_type: "type_of(u)=bool & default_val(u)=0"
+axiomatization where --{** Type declarations **}
+ p_type: "type_of(p)=bool & default_val(p)=0" and
+ m_type: "type_of(m)=int & default_val(m)=#0" and
+ n_type: "type_of(n)=int & default_val(n)=#0" and
+ u_type: "type_of(u)=bool & default_val(u)=0" and
v_type: "type_of(v)=bool & default_val(v)=0"
definition
--- a/src/ZF/ZF.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/ZF/ZF.thy Sat Feb 19 08:39:05 2011 +0100
@@ -207,21 +207,21 @@
subset_def: "A <= B == \<forall>x\<in>A. x\<in>B"
-axioms
+axiomatization where
(* ZF axioms -- see Suppes p.238
Axioms for Union, Pow and Replace state existence only,
uniqueness is derivable using extensionality. *)
- extension: "A = B <-> A <= B & B <= A"
- Union_iff: "A \<in> Union(C) <-> (\<exists>B\<in>C. A\<in>B)"
- Pow_iff: "A \<in> Pow(B) <-> A <= B"
+ extension: "A = B <-> A <= B & B <= A" and
+ Union_iff: "A \<in> Union(C) <-> (\<exists>B\<in>C. A\<in>B)" and
+ Pow_iff: "A \<in> Pow(B) <-> A <= B" and
(*We may name this set, though it is not uniquely defined.*)
- infinity: "0\<in>Inf & (\<forall>y\<in>Inf. succ(y): Inf)"
+ infinity: "0\<in>Inf & (\<forall>y\<in>Inf. succ(y): Inf)" and
(*This formulation facilitates case analysis on A.*)
- foundation: "A=0 | (\<exists>x\<in>A. \<forall>y\<in>x. y~:A)"
+ foundation: "A=0 | (\<exists>x\<in>A. \<forall>y\<in>x. y~:A)" and
(*Schema axiom since predicate P is a higher-order variable*)
replacement: "(\<forall>x\<in>A. \<forall>y z. P(x,y) & P(x,z) --> y=z) ==>
--- a/src/ZF/ex/Commutation.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/ZF/ex/Commutation.thy Sat Feb 19 08:39:05 2011 +0100
@@ -1,4 +1,4 @@
-(* Title: HOL/Lambda/Commutation.thy
+(* Title: ZF/ex/Commutation.thy
Author: Tobias Nipkow & Sidi Ould Ehmety
Copyright 1995 TU Muenchen
--- a/src/ZF/ex/LList.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/ZF/ex/LList.thy Sat Feb 19 08:39:05 2011 +0100
@@ -43,11 +43,9 @@
lconst :: "i => i" where
"lconst(a) == lfp(univ(a), %l. LCons(a,l))"
-consts
- flip :: "i => i"
-axioms
- flip_LNil: "flip(LNil) = LNil"
-
+axiomatization flip :: "i => i"
+where
+ flip_LNil: "flip(LNil) = LNil" and
flip_LCons: "[| x \<in> bool; l \<in> llist(bool) |]
==> flip(LCons(x,l)) = LCons(not(x), flip(l))"
--- a/src/ZF/ex/NatSum.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/ZF/ex/NatSum.thy Sat Feb 19 08:39:05 2011 +0100
@@ -1,4 +1,4 @@
-(* Title: ZF/ex/Natsum.thy
+(* Title: ZF/ex/NatSum.thy
Author: Tobias Nipkow & Lawrence C Paulson
A summation operator. sum(f,n+1) is the sum of all f(i), i=0...n.
--- a/src/ZF/pair.thy Thu Feb 17 09:31:29 2011 +0100
+++ b/src/ZF/pair.thy Sat Feb 19 08:39:05 2011 +0100
@@ -1,4 +1,4 @@
-(* Title: ZF/pair
+(* Title: ZF/pair.thy
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
Copyright 1992 University of Cambridge