[Ballarin1999] Clemens Ballarin, Computer Algebra and Theorem Proving, Author's PhD thesis, 1999. -
Last modified on $Date$ -
diff -r 2ff3a5589b05 -r 90a598019aeb src/HOL/Auth/Guard/README.html --- a/src/HOL/Auth/Guard/README.html Tue Mar 12 21:59:48 2013 +0100 +++ b/src/HOL/Auth/Guard/README.html Tue Mar 12 22:22:05 2013 +0100 @@ -1,7 +1,5 @@ - - diff -r 2ff3a5589b05 -r 90a598019aeb src/HOL/Auth/README.html --- a/src/HOL/Auth/README.html Tue Mar 12 21:59:48 2013 +0100 +++ b/src/HOL/Auth/README.html Tue Mar 12 22:22:05 2013 +0100 @@ -1,7 +1,5 @@ - - @@ -46,9 +44,6 @@Frederic Blanqui has contributed a theory of guardedness, which is demonstrated by proofs of some roving agent protocols. -
Last modified $Date$ -
Larry Paulson, diff -r 2ff3a5589b05 -r 90a598019aeb src/HOL/TLA/README.html --- a/src/HOL/TLA/README.html Tue Mar 12 21:59:48 2013 +0100 +++ b/src/HOL/TLA/README.html Tue Mar 12 22:22:05 2013 +0100 @@ -1,7 +1,5 @@ - - diff -r 2ff3a5589b05 -r 90a598019aeb src/HOL/UNITY/Comp/README.html --- a/src/HOL/UNITY/Comp/README.html Tue Mar 12 21:59:48 2013 +0100 +++ b/src/HOL/UNITY/Comp/README.html Tue Mar 12 22:22:05 2013 +0100 @@ -1,7 +1,5 @@ - - @@ -40,9 +38,6 @@ level of automation appears to be about the same as in HOL-UNITY by Flemming Andersen et al. -Last modified on $Date$ -
lcp@cl.cam.ac.uk diff -r 2ff3a5589b05 -r 90a598019aeb src/HOL/UNITY/README.html --- a/src/HOL/UNITY/README.html Tue Mar 12 21:59:48 2013 +0100 +++ b/src/HOL/UNITY/README.html Tue Mar 12 22:22:05 2013 +0100 @@ -1,7 +1,5 @@ - - @@ -45,9 +43,6 @@ The directoryComp
presents examples of proofs involving program composition.
-Last modified on $Date$ -
lcp@cl.cam.ac.uk diff -r 2ff3a5589b05 -r 90a598019aeb src/HOL/UNITY/Simple/README.html --- a/src/HOL/UNITY/Simple/README.html Tue Mar 12 21:59:48 2013 +0100 +++ b/src/HOL/UNITY/Simple/README.html Tue Mar 12 22:22:05 2013 +0100 @@ -1,7 +1,5 @@ - - @@ -37,9 +35,6 @@Reachability.thy)
-Last modified on $Date$ -
lcp@cl.cam.ac.uk